EmptyMS I c= M by MBOOLEAN:5;
then EmptyMS I in bool M by MBOOLEAN:1;
then reconsider a = EmptyMS I as Element of bool M by MSSUBFAM:11;
take a ; :: thesis: ( a is empty-yielding & a is finite-yielding )
thus ( a is empty-yielding & a is finite-yielding ) ; :: thesis: verum