---

Step * 1 1 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. B(Xac)
6. d : {p:Point| B(OXp)} 
7. B(Xbd)
⊢ Ax ∈ a + b ≤ c + d
BY
{ Assert ⌜a + b ≤ c + d⌝⋅ }

1
.....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

2
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. a + b ≤ c + d
⊢ 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.  B(Xac)
6.  d  :  \{p:Point|  B(OXp)\} 
7.  B(Xbd)
\mvdash{}  Ax  \mmember{}  a  +  b  \mleq{}  c  +  d


By

---

Latex:
Assert  \mkleeneopen{}a  +  b  \mleq{}  c  +  d\mkleeneclose{}\mcdot{}

---

Home Index