---

Step * of Lemma colinear-lsep-cycle

∀g:EuclideanPlane. ∀a,b,c,y:Point.  (a # bc ⇒ y ≠ b ⇒ Colinear(a;b;y) ⇒ y # bc)
BY
{ (InstLemma `colinear-lsep` [] THEN RepeatFor 8 ((ParallelLast' THENA Auto))) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;y)  {}\mRightarrow{}  y  \#  bc)


By

---

Latex:
(InstLemma  `colinear-lsep`  []  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto)))

---

Home Index