---

Step * 1 1 of Lemma geo-add-length_functionality_wrt_le


1. e : BasicGeometry
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. c : {p:Point| B(OXp)} 
5. a ≤ c
6. d : {p:Point| B(OXp)} 
7. b ≤ d
⊢ Ax ∈ a + b ≤ c + d
BY
{ (D -3 THEN D -1 THEN ExRepD) }

1
1. e : BasicGeometry
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. c : {p:Point| B(OXp)} 
5. p1 : {p:Point| B(OXp)} 
6. q1 : {p:Point| B(OXp)} 
7. p1 = a ∈ Length
8. q1 = c ∈ Length
9. B(Xp1q1)
10. d : {p:Point| B(OXp)} 
11. p' : {p:Point| B(OXp)} 
12. q' : {p:Point| B(OXp)} 
13. p' = b ∈ Length
14. q' = d ∈ Length
15. B(Xp'q')
⊢ Ax ∈ a + b ≤ c + d

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -3  THEN  D  -1  THEN  ExRepD)

---

Home Index