---

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