---

Step * 1 of Lemma stable__geo-le


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)
BY
{ ((GenConcl ⌜x = a ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜y = b ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN All (Unfold `geo-le`)
   THEN MemTypeCD) }

1
1. e : BasicGeometry
2. a : {p:Point| O_X_p} 
3. b : {p:Point| O_X_p} 
4. ¬¬↓∃p',q':{p:Point| O_X_p} . ((p' = a ∈ Length) ∧ (q' = b ∈ Length) ∧ X_p'_q')
⊢ ∃p',q':{p:Point| O_X_p} . ((p' = a ∈ Length) ∧ (q' = b ∈ Length) ∧ X_p'_q')

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  \{p:Point|  O\_X\_p\} 
6.  x1  \mmember{}  \{p:Point|  O\_X\_p\} 
7.  x  \mequiv{}  x1
8.  y  :  Base
9.  y1  :  Base
10.  y  =  y1
11.  y  \mmember{}  \{p:Point|  O\_X\_p\} 
12.  y1  \mmember{}  \{p:Point|  O\_X\_p\} 
13.  y  \mequiv{}  y1
\mvdash{}  (\mneg{}\mneg{}x  \mleq{}  y)  {}\mRightarrow{}  (Ax  \mmember{}  x  \mleq{}  y)


By

---

Latex:
((GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}y  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  All  (Unfold  `geo-le`)
  THEN  MemTypeCD)

---

Home Index