Step
*
of Lemma
null_mset_wf_f
∀s:DSet. (0{s} ∈ FiniteSet{s})
BY
{ ((D 0 THENM MemTypeCD) THEN Auto) }
Latex:
Latex:
\mforall{}s:DSet.  (0\{s\}  \mmember{}  FiniteSet\{s\})
By
Latex:
((D  0  THENM  MemTypeCD)  THEN  Auto)
Home
Index