let X, Y be set ; :: thesis: ( X \ Y = {} iff X c= Y )
thus ( X \ Y = {} implies X c= Y ) by XBOOLE_0:def 5; :: thesis: ( X c= Y implies X \ Y = {} )
assume A1: X c= Y ; :: thesis: X \ Y = {}
now :: thesis: for x being object holds
( x in X \ Y iff x in {} )
let x be object ; :: thesis: ( x in X \ Y iff x in {} )
( ( x in X & not x in Y ) iff contradiction ) by A1;
hence ( x in X \ Y iff x in {} ) by XBOOLE_0:def 5; :: thesis: verum
end;
hence X \ Y = {} by TARSKI:2; :: thesis: verum