reconsider x = {} as SubsetFamily of M by XBOOLE_1:2;
take x ; :: thesis: ( x is empty & x is finite )
thus ( x is empty & x is finite ) ; :: thesis: verum