---

Step * of Lemma geo-le_witness

∀[e:BasicGeometry]. ∀[p,q:{p:Point| O_X_p} ].  Ax ∈ p ≤ q supposing X_p_q
BY
{ TACTIC:((D 0 THENA Auto)
          THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
                      Auto)
          THEN Auto
          THEN Unfold `geo-le` 0
          THEN MemTypeCD) }

1
1. e : BasicGeometry
2. {p:Point| O_X_p}  ⊆r Length
3. p : {p:Point| O_X_p} 
4. q : {p:Point| O_X_p} 
5. X_p_q
⊢ ∃p',q':{p:Point| O_X_p} . ((p' = p ∈ Length) ∧ (q' = q ∈ Length) ∧ X_p'_q')

---

Latex:

---

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


By

---

Latex:
TACTIC:((D  0  THENA  Auto)
                THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                                        Auto)
                THEN  Auto
                THEN  Unfold  `geo-le`  0
                THEN  MemTypeCD)

---

Home Index