---

Step * of Lemma circle-strict-overlap-implies-overlap

No Annotations
∀g:GeometryPrimitives. (BasicGeometryAxioms(g) ⇒ (∀a,b,c,d:Point.  (StrictOverlap(a;b;c;d) ⇒ Overlap(a;b;c;d))))
BY
{ ((Auto THEN Unfold `circle-strict-overlap` -1 THEN Unfold `circle-overlap` 0)
   THEN D -1
   THEN (D 0 THEN ExRepD)
   THEN InstConcl [⌜p⌝;⌜q⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:GeometryPrimitives
    (BasicGeometryAxioms(g)  {}\mRightarrow{}  (\mforall{}a,b,c,d:Point.    (StrictOverlap(a;b;c;d)  {}\mRightarrow{}  Overlap(a;b;c;d))))


By

---

Latex:
((Auto  THEN  Unfold  `circle-strict-overlap`  -1  THEN  Unfold  `circle-overlap`  0)
  THEN  D  -1
  THEN  (D  0  THEN  ExRepD)
  THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index