---

Step * of Lemma prank_functionality

∀[P,Q:formula()].  prank(P) ≤ prank(Q) supposing P ⊆ Q
BY
{ (Auto THEN (FLemma `prank-psub` [-1] THENA Auto) THEN SplitOrHyps THEN Auto THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P,Q:formula()].    prank(P)  \mleq{}  prank(Q)  supposing  P  \msubseteq{}  Q


By

---

Latex:
(Auto
  THEN  (FLemma  `prank-psub`  [-1]  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index