---

Step * of Lemma eu-nontrivial_wf

∀[e:EuclideanStructure]
  (eu-nontrivial(e) ∈ {triple:Point × Point × Point| let a,b,c = triple in (¬(a = b ∈ Point)) ∧ (¬Colinear(a;b;c))} )
BY
{ (ProveWfLemma THEN All (Unfolds ``eu-point eu-colinear``)⋅ THEN DRecord 1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:EuclideanStructure]
    (eu-nontrivial(e)  \mmember{}  \{triple:Point  \mtimes{}  Point  \mtimes{}  Point| 
                                              let  a,b,c  =  triple  in 
                                              (\mneg{}(a  =  b))  \mwedge{}  (\mneg{}Colinear(a;b;c))\}  )


By

---

Latex:
(ProveWfLemma  THEN  All  (Unfolds  ``eu-point  eu-colinear``)\mcdot{}  THEN  DRecord  1  THEN  Auto)

---

Home Index