Step
*
of Lemma
geo-not-not-colinear
∀e:BasicGeometry. ∀[a,b,c:Point]. (¬¬Colinear(a;b;c)
⇐⇒ ¬¬(a_b_c ∨ b_c_a ∨ c_a_b))
BY
{ ((UnivCD THENA Auto) THEN RWO "geo-not-colinear<" 0 THEN Auto) }
Latex:
Latex:
\mforall{}e:BasicGeometry. \mforall{}[a,b,c:Point]. (\mneg{}\mneg{}Colinear(a;b;c) \mLeftarrow{}{}\mRightarrow{} \mneg{}\mneg{}(a\_b\_c \mvee{} b\_c\_a \mvee{} c\_a\_b))
By
Latex:
((UnivCD THENA Auto) THEN RWO "geo-not-colinear<" 0 THEN Auto)
Home
Index