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