[0] I c= M by MBOOLEAN:5;
then [0] I in bool M by MBOOLEAN:1;
then reconsider a = [0] 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