---

Step * 1 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
7. (z)↓
8. ∀a,b:Base.  (if z = Ax then a otherwise b ~ b)
⊢ z = Ax ∈ Base
BY
{ (Assert ⌜isaxiom(Ax) ≤ isaxiom(z)⌝⋅ THEN Auto THEN Reduce (-1) THEN (RWO "-2" (-1) THENA 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)
9. tt ≤ ff
⊢ 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
7.  (z)\mdownarrow{}
8.  \mforall{}a,b:Base.    (if  z  =  Ax  then  a  otherwise  b  \msim{}  b)
\mvdash{}  z  =  Ax


By

---

Latex:
(Assert  \mkleeneopen{}isaxiom(Ax)  \mleq{}  isaxiom(z)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Reduce  (-1)  THEN  (RWO  "-2"  (-1)  THENA  Auto))

---

Home Index