---

Step * 1 1 1 1 1 of Lemma geo-add-length_functionality_wrt_le

.....assertion..... 
1. e : BasicGeometry
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. c : {p:Point| B(OXp)} 
5. B(Xac)
6. d : {p:Point| B(OXp)} 
7. B(Xbd)
⊢ a + b ≤ c + d
BY
{ (RepUR ``geo-le geo-add-length`` 0 THEN (GeneralizeGeoExtends [`u';`w'] THENA Auto)) }

1
1. e : BasicGeometry
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. c : {p:Point| B(OXp)} 
5. B(Xac)
6. d : {p:Point| B(OXp)} 
7. B(Xbd)
8. u : {x:Point| B(Oax) ∧ ax ≅ Xb} 
9. au ≅ Xb ∧ B(Oau)
10. w : {x:Point| B(Ocx) ∧ cx ≅ Xd} 
11. cw ≅ Xd ∧ B(Ocw)
⊢ ↓∃p',q':{p:Point| B(OXp)} . ((p' = u ∈ Length) ∧ (q' = w ∈ Length) ∧ B(Xp'q'))

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  BasicGeometry
2.  a  :  \{p:Point|  B(OXp)\} 
3.  b  :  \{p:Point|  B(OXp)\} 
4.  c  :  \{p:Point|  B(OXp)\} 
5.  B(Xac)
6.  d  :  \{p:Point|  B(OXp)\} 
7.  B(Xbd)
\mvdash{}  a  +  b  \mleq{}  c  +  d


By

---

Latex:
(RepUR  ``geo-le  geo-add-length``  0  THEN  (GeneralizeGeoExtends  [`u';`w']  THENA  Auto))

---

Home Index