---

Step * of Lemma not_functionality_wrt_uimplies

∀[P,Q:ℙ].  ({P supposing Q} ⇒ {¬Q supposing ¬P})
BY
{ (Unfolds ``not guard`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbP{}].    (\{P  supposing  Q\}  {}\mRightarrow{}  \{\mneg{}Q  supposing  \mneg{}P\})


By

---

Latex:
(Unfolds  ``not  guard``  0  THEN  Auto)

---

Home Index