---

Step * 1 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
19. a ∈ Length
20. b ∈ Length
⊢ ∃p',q':{p:Point| O_X_p} . ((p' = a ∈ Length) ∧ (q' = b ∈ Length) ∧ X_p'_q')
BY
{ (InstConcl [⌜a⌝;⌜b⌝]⋅ THENA (Try (MemCD) 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
⊢ (a = a ∈ Length) ∧ (b = b ∈ Length) ∧ X_a_b

---

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
19.  a  \mmember{}  Length
20.  b  \mmember{}  Length
\mvdash{}  \mexists{}p',q':\{p:Point|  O\_X\_p\}  .  ((p'  =  a)  \mwedge{}  (q'  =  b)  \mwedge{}  X\_p'\_q')


By

---

Latex:
(InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  (Try  (MemCD)  THEN  Auto))

---

Home Index