---

Step * 1 1 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)
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'))
BY
{ ((Assert u ∈ {p:Point| B(OXp)}  BY Auto) THEN (Assert w ∈ {p:Point| B(OXp)}  BY 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)
12. u ∈ {p:Point| B(OXp)} 
13. w ∈ {p:Point| B(OXp)} 
⊢ ↓∃p',q':{p:Point| B(OXp)} . ((p' = u ∈ Length) ∧ (q' = w ∈ Length) ∧ B(Xp'q'))

---

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.  u  :  \{x:Point|  B(Oax)  \mwedge{}  ax  \mcong{}  Xb\} 
9.  au  \mcong{}  Xb  \mwedge{}  B(Oau)
10.  w  :  \{x:Point|  B(Ocx)  \mwedge{}  cx  \mcong{}  Xd\} 
11.  cw  \mcong{}  Xd  \mwedge{}  B(Ocw)
\mvdash{}  \mdownarrow{}\mexists{}p',q':\{p:Point|  B(OXp)\}  .  ((p'  =  u)  \mwedge{}  (q'  =  w)  \mwedge{}  B(Xp'q'))


By

---

Latex:
((Assert  u  \mmember{}  \{p:Point|  B(OXp)\}    BY  Auto)  THEN  (Assert  w  \mmember{}  \{p:Point|  B(OXp)\}    BY  Auto))

---

Home Index