Step
*
of Lemma
test-colinear-sets
∀e:BasicGeometry. ∀A,B,C,X,Y,Z,W,U,V:Point.  (A ≠ B 
⇒ Colinear(A;B;X) 
⇒ A_B_C 
⇒ Y_C_A 
⇒ Y ≠ C 
⇒ Colinear(C;Y;X))
BY
{ Auto }
Latex:
Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,X,Y,Z,W,U,V:Point.
    (A  \mneq{}  B  {}\mRightarrow{}  Colinear(A;B;X)  {}\mRightarrow{}  A\_B\_C  {}\mRightarrow{}  Y\_C\_A  {}\mRightarrow{}  Y  \mneq{}  C  {}\mRightarrow{}  Colinear(C;Y;X))
By
Latex:
Auto
Home
Index