---

Step * of Lemma subtype_rel_b-union_iff

∀[A,B,C:Type].  uiff((B ⋃ C) ⊆r A;(B ⊆r A) ∧ (C ⊆r A))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. C : Type
4. B ⊆r A
5. C ⊆r A
⊢ (B ⋃ C) ⊆r A

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    uiff((B  \mcup{}  C)  \msubseteq{}r  A;(B  \msubseteq{}r  A)  \mwedge{}  (C  \msubseteq{}r  A))


By

---

Latex:
Auto

---

Home Index