---

Step * 1 1 1 1 2 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)
8. a + b ≤ c + d
⊢ Ax ∈ a + b ≤ c + d
BY
{ (All (Unfold `geo-le`) THEN D -1 THEN MemTypeCD THEN Trivial) }

---

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)
8.  a  +  b  \mleq{}  c  +  d
\mvdash{}  Ax  \mmember{}  a  +  b  \mleq{}  c  +  d


By

---

Latex:
(All  (Unfold  `geo-le`)  THEN  D  -1  THEN  MemTypeCD  THEN  Trivial)

---

Home Index