---

Step * 1 1 1 1 1 1 1 1 of Lemma geo-add-length-cancel-left-le


1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. c + a ∈ {p:Point| O_X_p} 
9. c + b ∈ {p:Point| O_X_p} 
10. c + a ∈ {p:Point| O_X_p} 
11. c + b ∈ {p:Point| O_X_p} 
12. z : {x:Point| O_c_x ∧ cx ≅ Xa} 
13. cz ≅ Xa
14. O_c_z
15. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
16. cu ≅ Xb
17. O_c_u
18. X_z_u
⊢ ∃p',q':{p:Point| O_X_p} . ((p' = a ∈ Length) ∧ (q' = b ∈ Length) ∧ X_p'_q')
BY
{ ((Assert a ∈ Length BY
          (SubsumeC ⌜{p:Point| O_X_p} ⌝⋅ THEN Auto))
   THEN (Assert b ∈ Length BY
               (SubsumeC ⌜{p:Point| O_X_p} ⌝⋅ THEN Auto))
   ) }

1
1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. c + a ∈ {p:Point| O_X_p} 
9. c + b ∈ {p:Point| O_X_p} 
10. c + a ∈ {p:Point| O_X_p} 
11. c + b ∈ {p:Point| O_X_p} 
12. z : {x:Point| O_c_x ∧ cx ≅ Xa} 
13. cz ≅ Xa
14. O_c_z
15. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
16. cu ≅ Xb
17. O_c_u
18. X_z_u
19. a ∈ Length
20. b ∈ Length
⊢ ∃p',q':{p:Point| O_X_p} . ((p' = a ∈ Length) ∧ (q' = b ∈ Length) ∧ X_p'_q')

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  O\_X\_a
4.  b  :  Point
5.  O\_X\_b
6.  c  :  Point
7.  O\_X\_c
8.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
9.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
10.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
11.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
12.  z  :  \{x:Point|  O\_c\_x  \mwedge{}  cx  \00D0  Xa\} 
13.  cz  \00D0  Xa
14.  O\_c\_z
15.  u  :  \{x:Point|  O\_c\_x  \mwedge{}  cx  \00D0  Xb\} 
16.  cu  \00D0  Xb
17.  O\_c\_u
18.  X\_z\_u
\mvdash{}  \mexists{}p',q':\{p:Point|  O\_X\_p\}  .  ((p'  =  a)  \mwedge{}  (q'  =  b)  \mwedge{}  X\_p'\_q')


By

---

Latex:
((Assert  a  \mmember{}  Length  BY
                (SubsumeC  \mkleeneopen{}\{p:Point|  O\_X\_p\}  \mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  b  \mmember{}  Length  BY
                          (SubsumeC  \mkleeneopen{}\{p:Point|  O\_X\_p\}  \mkleeneclose{}\mcdot{}  THEN  Auto))
  )

---

Home Index