set M = multiples 0;
thus multiples 0 c= {0} :: according to XBOOLE_0:def 10 :: thesis: {0} c= multiples 0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in multiples 0 or x in {0} )
assume x in multiples 0 ; :: thesis: x in {0}
then reconsider m = x as Multiple of 0 by Th61;
0 divides m by Def15;
hence x in {0} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0} or x in multiples 0 )
assume x in {0} ; :: thesis: x in multiples 0
then A1: x = 0 ;
0 is Multiple of 0 by Def15;
hence x in multiples 0 by A1; :: thesis: verum