---

Step * 2 of Lemma geo-le-iff


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. P : Point
6. CP ≥ AB
⊢ |AB| ≤ |CP|
BY
{ ((D 0 THEN RepUR ``geo-length`` 0 THEN GeneralizeGeoExtends [`ab'; `cp'])
   THEN (Assert {p:Point| B(OXp)}  ⊆r Length BY
               Auto)
   ) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. P : Point
6. CP ≥ AB
7. ab : {x:Point| B(OXx) ∧ Xx ≅ AB} 
8. Xab ≅ AB ∧ B(OXab)
9. cp : {x:Point| B(OXx) ∧ Xx ≅ CP} 
10. Xcp ≅ CP ∧ B(OXcp)
11. {p:Point| B(OXp)}  ⊆r Length
⊢ ∃p',q':{p:Point| B(OXp)} . ((p' = ab ∈ Length) ∧ (q' = cp ∈ Length) ∧ B(Xp'q'))

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  P  :  Point
6.  CP  \mgeq{}  AB
\mvdash{}  |AB|  \mleq{}  |CP|


By

---

Latex:
((D  0  THEN  RepUR  ``geo-length``  0  THEN  GeneralizeGeoExtends  [`ab';  `cp'])
  THEN  (Assert  \{p:Point|  B(OXp)\}    \msubseteq{}r  Length  BY
                          Auto)
  )

---

Home Index