---

Step * of Lemma geo-le_imp

∀e:BasicGeometry. ∀p,q:{p:Point| O_X_p} .  X_p_q supposing p ≤ q
BY
{ (Intros
   THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
               Auto)
   THEN (Unhide THENA Auto)
   THEN D -2
   THEN (Unhide THENA Auto)
   THEN ExRepD) }

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 ∈ Length
7. q' = q ∈ Length
8. X_p'_q'
9. {p:Point| O_X_p}  ⊆r Length
⊢ X_p_q

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q:\{p:Point|  O\_X\_p\}  .    X\_p\_q  supposing  p  \mleq{}  q


By

---

Latex:
(Intros
  THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                          Auto)
  THEN  (Unhide  THENA  Auto)
  THEN  D  -2
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD)

---

Home Index