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