---

Step * of Lemma isaxiom-implies-not-isint

∀[t:Base]. (¬↑isint(t)) supposing ((↑isaxiom(t)) and (t)↓)
BY
{ (CanonicalAuto
   THEN (Assert ⌜↑isint(t)⌝⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN CanonicalAuto
   THEN HypSubst (-1) (-2)
   THEN Reduce (-2)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (\mneg{}\muparrow{}isint(t))  supposing  ((\muparrow{}isaxiom(t))  and  (t)\mdownarrow{})


By

---

Latex:
(CanonicalAuto
  THEN  (Assert  \mkleeneopen{}\muparrow{}isint(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  CanonicalAuto
  THEN  HypSubst  (-1)  (-2)
  THEN  Reduce  (-2)
  THEN  Trivial)

---

Home Index