---

Step * 1 1 of Lemma isaxiom-sqequal


1. C : Base
2. strict(C)
3. A : Base
4. B : Base
5. z : Base
6. (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(if z = Ax then A z otherwise B z)
8. is-exception(z)
9. u : Base
10. v : Base
11. z ~ exception(u; v)
⊢ exception(u; v) ≤ C (exception(u; v))
BY
{ ((D 2 THEN Auto) THEN RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Base
2.  strict(C)
3.  A  :  Base
4.  B  :  Base
5.  z  :  Base
6.  (A  Ax  \msim{}  C  Ax)  \mwedge{}  ((\mforall{}a,b:Base.    (if  z  =  Ax  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z))
7.  is-exception(if  z  =  Ax  then  A  z  otherwise  B  z)
8.  is-exception(z)
9.  u  :  Base
10.  v  :  Base
11.  z  \msim{}  exception(u;  v)
\mvdash{}  exception(u;  v)  \mleq{}  C  (exception(u;  v))


By

---

Latex:
((D  2  THEN  Auto)  THEN  RWO  "3"  0  THEN  Auto)

---

Home Index