---

Step * of Lemma geo-CCL_wf

No Annotations
∀[g:EuclideanPlaneStructure]
  (BasicGeometryAxioms(g)
  ⇒ (∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:Point.
        CCL(a;b;c;d) ∈ {u:Point| ab ≅ au ∧ cd ≅ cu ∧ u leftof ac}  supposing ∃p,q:Point. ((ab ≅ ap ∧ cd>cp) ∧ cd ≅ cq ∧ \000Cab>aq)))
BY
{ (InstLemma `geo-CC_wf` []
   THEN ((ParallelLast' THEN (D 0 THENA Auto)) THEN Auto)
   THEN (Assert StrictOverlap(a;b;c;d) BY
               (D 0 THEN Auto))
   THEN ((Assert Overlap(a;b;c;d) BY
                (InstLemma  `circle-strict-overlap-implies-overlap` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THEN Auto))
   THENM ProveWfLemma
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:EuclideanPlaneStructure]
    (BasicGeometryAxioms(g)
    {}\mRightarrow{}  (\mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:Point.
                CCL(a;b;c;d)  \mmember{}  \{u:Point|  ab  \mcong{}  au  \mwedge{}  cd  \mcong{}  cu  \mwedge{}  u  leftof  ac\}   
                supposing  \mexists{}p,q:Point.  ((ab  \mcong{}  ap  \mwedge{}  cd>cp)  \mwedge{}  cd  \mcong{}  cq  \mwedge{}  ab>aq)))


By

---

Latex:
(InstLemma  `geo-CC\_wf`  []
  THEN  ((ParallelLast'  THEN  (D  0  THENA  Auto))  THEN  Auto)
  THEN  (Assert  StrictOverlap(a;b;c;d)  BY
                          (D  0  THEN  Auto))
  THEN  ((Assert  Overlap(a;b;c;d)  BY
                            (InstLemma    `circle-strict-overlap-implies-overlap`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THENM  ProveWfLemma
  ))

---

Home Index