---

Step * of Lemma geo-lt-implies-point

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (|ab| < |cd| ⇒ a ≠ b ⇒ (∃f:Point. (a-b-f ∧ af ≅ cd)))
BY
{ (Auto
   THEN (InstLemma  `geo-lt-implies-gt-strong-1` [⌜e⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN ((gProperProlong ⌜a⌝⌜b⌝`g'⌜w⌝⌜d⌝⋅ THENA Auto) THEN ExRepD)
   THEN D 0 With ⌜g⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (|ab|  <  |cd|  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}f:Point.  (a-b-f  \mwedge{}  af  \mcong{}  cd)))


By

---

Latex:
(Auto
  THEN  (InstLemma    `geo-lt-implies-gt-strong-1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  ((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`g'\mkleeneopen{}w\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  D  0  With  \mkleeneopen{}g\mkleeneclose{} 
  THEN  Auto)

---

Home Index