---

Step * of Lemma lsep-not-between

∀g:OrientedPlane. ∀a,b,c:Point.  (a # bc ⇒ (¬a_b_c))
BY
{ (Auto
   THEN (D -1
         THENL [(RepeatFor 2 ((FLemma `left-symmetry` [-1] THENA Auto)) THEN FLemma `left-not-between` [-1] THEN Auto)
               ; (FLemma `left-not-between` [-1] THEN Auto)]
        )
   ) }

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}a\_b\_c))


By

---

Latex:
(Auto
  THEN  (D  -1
              THENL  [(RepeatFor  2  ((FLemma  `left-symmetry`  [-1]  THENA  Auto))
                              THEN  FLemma  `left-not-between`  [-1]
                              THEN  Auto)
                          ;  (FLemma  `left-not-between`  [-1]  THEN  Auto)]
            )
  )

---

Home Index