set M = {} ;
reconsider M = {} as Subset of by XBOOLE_1:2;
reconsider M = M as cone Subset of by Th6;
take M ; :: thesis: ( M is empty & M is cone )
thus ( M is empty & M is cone ) ; :: thesis: verum