Step
*
of Lemma
eu-not-equal-OXY
∀[e:EuclideanStructure]. ((¬(O = X ∈ Point)) ∧ (¬(O = Y ∈ Point)) ∧ (¬(X = Y ∈ Point)))
BY
{ (InstLemma `eu-not-colinear-OXY` []⋅
THEN ParallelLast
THEN SplitAndConcl
THEN D 0
THEN Auto
THEN (D -2 THEN RevHypSubst (-1) 0 THEN Auto THEN RWO "eu-colinear-def" 0 THEN Auto)) }
Latex:
Latex:
\mforall{}[e:EuclideanStructure]. ((\mneg{}(O = X)) \mwedge{} (\mneg{}(O = Y)) \mwedge{} (\mneg{}(X = Y)))
By
Latex:
(InstLemma `eu-not-colinear-OXY` []\mcdot{}
THEN ParallelLast
THEN SplitAndConcl
THEN D 0
THEN Auto
THEN (D -2 THEN RevHypSubst (-1) 0 THEN Auto THEN RWO "eu-colinear-def" 0 THEN Auto))
Home
Index