---

Step * 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 ∈ Length
11. q' = c + b ∈ Length
12. X_p'_q'
13. c + a ∈ {p:Point| O_X_p} 
14. c + b ∈ {p:Point| O_X_p} 
⊢ Ax ∈ a ≤ b
BY
{ (((EqTypeHD (-5) THENA Auto) THEN (EliminatePoint (-5) THENA Auto))
   THEN (EqTypeHD (-4) THENA Auto)
   THEN (EliminatePoint (-4) THENA 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. 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. X_c + a_c + b
19. c + a ∈ {p:Point| O_X_p} 
20. c + b ∈ {p:Point| O_X_p} 
⊢ 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.  q'  =  c  +  b
12.  X\_p'\_q'
13.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
14.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
\mvdash{}  Ax  \mmember{}  a  \mleq{}  b


By

---

Latex:
(((EqTypeHD  (-5)  THENA  Auto)  THEN  (EliminatePoint  (-5)  THENA  Auto))
  THEN  (EqTypeHD  (-4)  THENA  Auto)
  THEN  (EliminatePoint  (-4)  THENA  Auto))

---

Home Index