---

Step * 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. 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
BY
{ (((EqTypeHD 7 THENA Auto) THEN (RWO "10" 12 THENA Auto) THEN ThinVar `p1')
   THEN ((EqTypeHD 7 THENA Auto) THEN (RWO "10" 11 THENA Auto) THEN ThinVar `q1')
   THEN ((EqTypeHD (-3) THENA Auto) THEN (RWO "-3" (-1) THENA Auto) THEN ThinVar `p\'')
   THEN ((EqTypeHD (-2) THENA Auto) THEN (RWO "-2" (-1) THENA Auto) THEN ThinVar `q\'')
   THEN RepeatFor 2 (Thin (-2))
   THEN RepeatFor 2 (Thin (-4))) }

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)
⊢ 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.  p1  :  \{p:Point|  B(OXp)\} 
6.  q1  :  \{p:Point|  B(OXp)\} 
7.  p1  =  a
8.  q1  =  c
9.  B(Xp1q1)
10.  d  :  \{p:Point|  B(OXp)\} 
11.  p'  :  \{p:Point|  B(OXp)\} 
12.  q'  :  \{p:Point|  B(OXp)\} 
13.  p'  =  b
14.  q'  =  d
15.  B(Xp'q')
\mvdash{}  Ax  \mmember{}  a  +  b  \mleq{}  c  +  d


By

---

Latex:
(((EqTypeHD  7  THENA  Auto)  THEN  (RWO  "10"  12  THENA  Auto)  THEN  ThinVar  `p1')
  THEN  ((EqTypeHD  7  THENA  Auto)  THEN  (RWO  "10"  11  THENA  Auto)  THEN  ThinVar  `q1')
  THEN  ((EqTypeHD  (-3)  THENA  Auto)  THEN  (RWO  "-3"  (-1)  THENA  Auto)  THEN  ThinVar  `p\mbackslash{}'')
  THEN  ((EqTypeHD  (-2)  THENA  Auto)  THEN  (RWO  "-2"  (-1)  THENA  Auto)  THEN  ThinVar  `q\mbackslash{}'')
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  RepeatFor  2  (Thin  (-4)))

---

Home Index