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

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