---

Step * of Lemma union_subtype_base

∀[A,B:Type].  ((A + B) ⊆r Base) supposing ((B ⊆r Base) and (A ⊆r Base))
BY
{ (Intros THEN (D 0 THENA Auto) THEN D -1 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index