---

Step * of Lemma lsep-iff

No Annotations
∀g:OrientedPlane. ∀a,b,c:Point.  (a # bc ⇐⇒ (∀y:Point. (y # b ⇒ Colinear(y;b;c) ⇒ a # by)) ∧ c # b)
BY
{ ((UnivCD THENA Auto) THEN (Assert Colinear(c;b;c) BY Auto) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:OrientedPlane.  \mforall{}a,b,c:Point.
    (a  \#  bc  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y:Point.  (y  \#  b  {}\mRightarrow{}  Colinear(y;b;c)  {}\mRightarrow{}  a  \#  by))  \mwedge{}  c  \#  b)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Assert  Colinear(c;b;c)  BY  Auto)  THEN  Auto)

---

Home Index