---

Step * of Lemma psub_weakening

∀a,b:formula().  a ⊆ b supposing a = b ∈ formula()
BY
{ xxx((D 0 THENA Auto)
      THEN (BLemma `formula-induction` THENA Auto)
      THEN Unfold `psub` 0
      THEN Reduce 0
      THEN Try (Fold `psub` 0)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}a,b:formula().    a  \msubseteq{}  b  supposing  a  =  b


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  (BLemma  `formula-induction`  THENA  Auto)
        THEN  Unfold  `psub`  0
        THEN  Reduce  0
        THEN  Try  (Fold  `psub`  0)
        THEN  Auto)xxx

---

Home Index