---

Step * of Lemma subtype_rel_b-union

∀[A1,B1,A2,B2:Type].  (A1 ⋃ B1) ⊆r (A2 ⋃ B2) supposing (A1 ⊆r A2) ∧ (B1 ⊆r B2)
BY
{ (Unfold `b-union` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A1,B1,A2,B2:Type].    (A1  \mcup{}  B1)  \msubseteq{}r  (A2  \mcup{}  B2)  supposing  (A1  \msubseteq{}r  A2)  \mwedge{}  (B1  \msubseteq{}r  B2)


By

---

Latex:
(Unfold  `b-union`  0  THEN  Auto)

---

Home Index