---

Step * 1 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 ∈ 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
BY
{ (Unhide THEN Auto THEN RWO "-7 -3" (-2) THEN Auto) }

---

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.  [\%]  :  (p'  \mmember{}  \{p:Point|  O\_X\_p\}  )  \mwedge{}  (p  \mmember{}  \{p:Point|  O\_X\_p\}  )  \mwedge{}  p'  \mequiv{}  p
8.  q'  =  q
9.  [\%9]  :  (q'  \mmember{}  \{p:Point|  O\_X\_p\}  )  \mwedge{}  (q  \mmember{}  \{p:Point|  O\_X\_p\}  )  \mwedge{}  q'  \mequiv{}  q
10.  X\_p'\_q'
11.  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length
\mvdash{}  X\_p\_q


By

---

Latex:
(Unhide  THEN  Auto  THEN  RWO  "-7  -3"  (-2)  THEN  Auto)

---

Home Index