---

Step * 1 of Lemma geo-le_imp


1. e : BasicGeometry
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. p' : {p:Point| O_X_p} 
5. q' : {p:Point| O_X_p} 
6. p' = p ∈ Length
7. q' = q ∈ Length
8. X_p'_q'
9. {p:Point| O_X_p}  ⊆r Length
⊢ X_p_q
BY
{ ((EqTypeHD (-4) THENA Auto) THEN (EqTypeHD (-3) THENA Auto) THEN Auto) }

1
1. e : BasicGeometry
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. p' : {p:Point| O_X_p} 
5. q' : {p:Point| O_X_p} 
6. p' = p ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
7. [%] : (p' ∈ {p:Point| O_X_p} ) ∧ (p ∈ {p:Point| O_X_p} ) ∧ p' ≡ p
8. q' = q ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
9. [%9] : (q' ∈ {p:Point| O_X_p} ) ∧ (q ∈ {p:Point| O_X_p} ) ∧ q' ≡ q
10. X_p'_q'
11. {p:Point| O_X_p}  ⊆r Length
⊢ X_p_q

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  p  :  \{p:Point|  O\_X\_p\} 
3.  q  :  \{p:Point|  O\_X\_p\} 
4.  p'  :  \{p:Point|  O\_X\_p\} 
5.  q'  :  \{p:Point|  O\_X\_p\} 
6.  p'  =  p
7.  q'  =  q
8.  X\_p'\_q'
9.  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length
\mvdash{}  X\_p\_q


By

---

Latex:
((EqTypeHD  (-4)  THENA  Auto)  THEN  (EqTypeHD  (-3)  THENA  Auto)  THEN  Auto)

---

Home Index