reconsider A = {} as Subset of X by XBOOLE_1:2;
take A ; :: thesis: ex B being set st
( B in S & A c= B & M . B = 0. )
take B = {} ; :: thesis: ( B in S & A c= B & M . B = 0. )
thus B in S by PROB_1:4; :: thesis: ( A c= B & M . B = 0. )
thus A c= B ; :: thesis: M . B = 0.
thus M . B = 0. by VALUED_0:def 19; :: thesis: verum