---

Step * of Lemma geo-CC_wf

No Annotations
∀[g:EuclideanPlaneStructure]. ∀[a,b:Point]. ∀[c:{c:Point| a # c} ]. ∀[d:{d:Point| StrictOverlap(a;b;c;d)} ].
  (CC(a;b;c;d) ∈ {u:Point| ab ≅ au ∧ cd ≅ cu ∧ u leftof ac} )
BY
{ (Auto THEN (D 1 THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:EuclideanPlaneStructure].  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  a  \#  c\}  ].  \mforall{}[d:\{d:Point| 
                                                                                                                                                StrictOverlap(a;b;c;d)\}  ].
    (CC(a;b;c;d)  \mmember{}  \{u:Point|  ab  \mcong{}  au  \mwedge{}  cd  \mcong{}  cu  \mwedge{}  u  leftof  ac\}  )


By

---

Latex:
(Auto  THEN  (D  1  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index