---

Step * of Lemma b-union-void

∀[V,T:Type].  ((V ⋃ T) ⊆r T) ∧ ((T ⋃ V) ⊆r T) supposing ¬V
BY
{ (Auto THEN D 0 THEN Auto THEN (D_b_union (-1) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[V,T:Type].    ((V  \mcup{}  T)  \msubseteq{}r  T)  \mwedge{}  ((T  \mcup{}  V)  \msubseteq{}r  T)  supposing  \mneg{}V


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  (D\_b\_union  (-1)  THEN  Auto)\mcdot{})

---

Home Index