---

Step * of Lemma not_subtype_rel

∀[A,B:Type].  (¬A) ⊆r (¬B) supposing B ⊆r A
BY
{ (Auto THEN All (Unfold `not`) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (\mneg{}A)  \msubseteq{}r  (\mneg{}B)  supposing  B  \msubseteq{}r  A


By

---

Latex:
(Auto  THEN  All  (Unfold  `not`)  THEN  Auto)

---

Home Index