---

Step * of Lemma geo-le_antisymmetry

∀e:BasicGeometry. ∀[p,q:Length].  (p = q ∈ Length) supposing (q ≤ p and p ≤ q)
BY
{ ((Intros THEN (Unhide THENA Auto))
   THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
               Auto)
   THEN DVar `p'
   THEN DVar `q'
   THEN EqTypeCD
   THEN Auto) }

1
.....antecedent..... 
1. e : BasicGeometry
2. p : Base
3. p1 : Base
4. p = p1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
5. p ∈ {p:Point| O_X_p} 
6. p1 ∈ {p:Point| O_X_p} 
7. p ≡ p1
8. q : Base
9. q1 : Base
10. q = q1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. q ∈ {p:Point| O_X_p} 
12. q1 ∈ {p:Point| O_X_p} 
13. q ≡ q1
14. p ≤ q
15. q ≤ p
16. {p:Point| O_X_p}  ⊆r Length
⊢ p ≡ q1

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p,q:Length].    (p  =  q)  supposing  (q  \mleq{}  p  and  p  \mleq{}  q)


By

---

Latex:
((Intros  THEN  (Unhide  THENA  Auto))
  THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                          Auto)
  THEN  DVar  `p'
  THEN  DVar  `q'
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index