---

Step * of Lemma test-colinear-sets

∀e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
  (Colinear(A;B;X) ⇒ A_B_C ⇒ Y_C_A ⇒ (¬(Y = C ∈ Point)) ⇒ Colinear(C;Y;X))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,X,Y,Z,W,U,V:Point.
    (Colinear(A;B;X)  {}\mRightarrow{}  A\_B\_C  {}\mRightarrow{}  Y\_C\_A  {}\mRightarrow{}  (\mneg{}(Y  =  C))  {}\mRightarrow{}  Colinear(C;Y;X))


By

---

Latex:
Auto

---

Home Index