---

Step * 1 of Lemma oriented-colinear-trans


1. ∀e:EuclideanPlane
     ∀[A,C,B,D:Point].  (Colinear(A;B;C) ⇒ Colinear(B;C;D) ⇒ B ≠ C ⇒ {Colinear(A;C;D) ∧ Colinear(A;B;D)})
⊢ OrientedPlane ~ EuclideanPlane
BY
{ (ByComputation 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}e:EuclideanPlane
          \mforall{}[A,C,B,D:Point].
              (Colinear(A;B;C)  {}\mRightarrow{}  Colinear(B;C;D)  {}\mRightarrow{}  B  \mneq{}  C  {}\mRightarrow{}  \{Colinear(A;C;D)  \mwedge{}  Colinear(A;B;D)\})
\mvdash{}  OrientedPlane  \msim{}  EuclideanPlane


By

---

Latex:
(ByComputation  0  THEN  Auto)

---

Home Index