---

Step * of Lemma geo-gt-prim-implies-le

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab>cd ⇒ |cd| ≤ |ab|)
BY
{ (Auto
   THEN (Unfold `geo-le` 0 THEN Auto)
   THEN (Assert a # b BY
               ((Unfold `geo-sep` 0 THENA Auto)
                THEN UseGeoAxioms
                THEN InstHyp [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜a⌝] (10)⋅
                THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab>cd
7. a # b
⊢ ↓∃p',q':{p:Point| B(OXp)} . ((p' = |cd| ∈ Length) ∧ (q' = |ab| ∈ Length) ∧ B(Xp'q'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  |cd|  \mleq{}  |ab|)


By

---

Latex:
(Auto
  THEN  (Unfold  `geo-le`  0  THEN  Auto)
  THEN  (Assert  a  \#  b  BY
                          ((Unfold  `geo-sep`  0  THENA  Auto)
                            THEN  UseGeoAxioms
                            THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (10)\mcdot{}
                            THEN  Auto)))

---

Home Index