---

Step * of Lemma lsep-all-sym2

∀g:EuclideanPlane. ∀a,b,c:Point.  (a leftof bc ⇒ {a # bc ∧ b # ca ∧ c # ab ∧ a # cb ∧ b # ac ∧ c # ba})
BY
{ (InstLemma `lsep-all-sym` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (Assert a # bc BY
               (OrLeft THEN Auto))
   THEN ThinTrivial
   THEN D -1
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.
    (a  leftof  bc  {}\mRightarrow{}  \{a  \#  bc  \mwedge{}  b  \#  ca  \mwedge{}  c  \#  ab  \mwedge{}  a  \#  cb  \mwedge{}  b  \#  ac  \mwedge{}  c  \#  ba\})


By

---

Latex:
(InstLemma  `lsep-all-sym`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  a  \#  bc  BY
                          (OrLeft  THEN  Auto))
  THEN  ThinTrivial
  THEN  D  -1
  THEN  D  0
  THEN  Auto)

---

Home Index