---

Step * of Lemma stable__geo-le

∀e:BasicGeometry. ∀x,y:Length.  Stable{x ≤ y}
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN All (Unfold  `geo-length-type`)
   THEN UseWitness ⌜Ax⌝⋅
   THEN (D 2 THEN D -2)
   THEN Fold `member` 0
   THEN MoveToConcl (-1)) }

1
1. e : BasicGeometry
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
5. x ∈ {p:Point| O_X_p} 
6. x1 ∈ {p:Point| O_X_p} 
7. x ≡ x1
8. y : Base
9. y1 : Base
10. y = y1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. y ∈ {p:Point| O_X_p} 
12. y1 ∈ {p:Point| O_X_p} 
13. y ≡ y1
⊢ (¬¬x ≤ y) ⇒ (Ax ∈ x ≤ y)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}x,y:Length.    Stable\{x  \mleq{}  y\}


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  All  (Unfold    `geo-length-type`)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  (D  2  THEN  D  -2)
  THEN  Fold  `member`  0
  THEN  MoveToConcl  (-1))

---

Home Index