---

Step * 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. p' : {p:Point| O_X_p} 
9. q' : {p:Point| O_X_p} 
10. p' = c + a ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. p' ∈ {p:Point| O_X_p} 
12. c + a ∈ {p:Point| O_X_p} 
13. p' ≡ c + a
14. q' = c + b ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
15. q' ∈ {p:Point| O_X_p} 
16. c + b ∈ {p:Point| O_X_p} 
17. q' ≡ c + b
18. c + a ∈ {p:Point| O_X_p} 
19. c + b ∈ {p:Point| O_X_p} 
20. z : {x:Point| O_c_x ∧ cx ≅ Xa} 
21. cz ≅ Xa ∧ O_c_z
22. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
23. cu ≅ Xb ∧ O_c_u
⊢ X_z_u ⇒ (Ax ∈ a ≤ b)
BY
{ (ThinVar `q\'' THEN ThinVar `p\'') }

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 ∧ O_c_z
14. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
15. cu ≅ Xb ∧ O_c_u
⊢ X_z_u ⇒ (Ax ∈ 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.  p'  :  \{p:Point|  O\_X\_p\} 
9.  q'  :  \{p:Point|  O\_X\_p\} 
10.  p'  =  c  +  a
11.  p'  \mmember{}  \{p:Point|  O\_X\_p\} 
12.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
13.  p'  \mequiv{}  c  +  a
14.  q'  =  c  +  b
15.  q'  \mmember{}  \{p:Point|  O\_X\_p\} 
16.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
17.  q'  \mequiv{}  c  +  b
18.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
19.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
20.  z  :  \{x:Point|  O\_c\_x  \mwedge{}  cx  \00D0  Xa\} 
21.  cz  \00D0  Xa  \mwedge{}  O\_c\_z
22.  u  :  \{x:Point|  O\_c\_x  \mwedge{}  cx  \00D0  Xb\} 
23.  cu  \00D0  Xb  \mwedge{}  O\_c\_u
\mvdash{}  X\_z\_u  {}\mRightarrow{}  (Ax  \mmember{}  a  \mleq{}  b)


By

---

Latex:
(ThinVar  `q\mbackslash{}''  THEN  ThinVar  `p\mbackslash{}'')

---

Home Index