Step
*
of Lemma
geo-col-out2-col
∀e:BasicGeometry. ∀a,b,c,a',c':Point.  (Colinear(a;b;c) 
⇒ out(b aa') 
⇒ out(b cc') 
⇒ Colinear(a';b;c'))
BY
{ Auto }
Latex:
Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',c':Point.
    (Colinear(a;b;c)  {}\mRightarrow{}  out(b  aa')  {}\mRightarrow{}  out(b  cc')  {}\mRightarrow{}  Colinear(a';b;c'))
By
Latex:
Auto
Home
Index