---

Step * 1 of Lemma is-above-axiom-general


1. T : Type
2. T ⊆r Base
3. z : Base
4. y : Base
5. y = Ax ∈ T
6. Ax ≤ z
⊢ z = Ax ∈ Base
BY
{ ((FLemma `has-value-monotonic` [-1] THENA (Reduce 0 THEN Auto))
   THEN ((FLemma `has-value-implies-dec-isaxiom-2` [-1]⋅ THENM D -1) THEN Auto)⋅
   )⋅ }

1
1. T : Type
2. T ⊆r Base
3. z : Base
4. y : Base
5. y = Ax ∈ T
6. Ax ≤ z
7. (z)↓
8. ∀a,b:Base.  (if z = Ax then a otherwise b ~ b)
⊢ z = Ax ∈ Base

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  z  :  Base
4.  y  :  Base
5.  y  =  Ax
6.  Ax  \mleq{}  z
\mvdash{}  z  =  Ax


By

---

Latex:
((FLemma  `has-value-monotonic`  [-1]  THENA  (Reduce  0  THEN  Auto))
  THEN  ((FLemma  `has-value-implies-dec-isaxiom-2`  [-1]\mcdot{}  THENM  D  -1)  THEN  Auto)\mcdot{}
  )\mcdot{}

---

Home Index