---

Step * 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 ∧ O_c_z
14. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
15. cu ≅ Xb ∧ O_c_u
⊢ X_z_u ⇒ (Ax ∈ a ≤ b)
BY
{ ((Auto THEN Unfold `geo-le` 0) THEN MemTypeCD) }

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
⊢ ∃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  \mwedge{}  O\_c\_z
14.  u  :  \{x:Point|  O\_c\_x  \mwedge{}  cx  \00D0  Xb\} 
15.  cu  \00D0  Xb  \mwedge{}  O\_c\_u
\mvdash{}  X\_z\_u  {}\mRightarrow{}  (Ax  \mmember{}  a  \mleq{}  b)


By

---

Latex:
((Auto  THEN  Unfold  `geo-le`  0)  THEN  MemTypeCD)

---

Home Index