---

Step * of Lemma not-dist-lemma

∀g:EuclideanPlane. ∀a,b,c,d:Point.  ((¬D(a;b;b;b;c;d)) ⇒ (¬ab > cd))
BY
{ ((Auto THEN (D 0 THENA Auto))
   THEN Unfold `geo-gt` -1
   THEN Unfold `dist` -2
   THEN D -1
   THEN D -2
   THEN (ExRepD THEN (InstConcl [⌜a⌝;⌜b⌝;⌜b⌝]⋅ THENA Auto))
   THEN D 0 With ⌜w⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    ((\mneg{}D(a;b;b;b;c;d))  {}\mRightarrow{}  (\mneg{}ab  >  cd))


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))
  THEN  Unfold  `geo-gt`  -1
  THEN  Unfold  `dist`  -2
  THEN  D  -1
  THEN  D  -2
  THEN  (ExRepD  THEN  (InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  D  0  With  \mkleeneopen{}w\mkleeneclose{} 
  THEN  Auto)

---

Home Index