let X, Y be set ; :: thesis: ( X \ Y = {} iff X c= Y )
thus ( X \ Y = {} implies X c= Y ) :: thesis: ( X c= Y implies X \ Y = {} )

proof

assume A1: X \ Y = {} ; :: thesis: X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume ( x in X & not x in Y ) ; :: thesis: contradiction
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

assume A2: X c= Y ; :: thesis: X \ Y = {}

now

let x be set ; :: thesis: ( x in X \ Y iff x in {} )
( ( x in X & not x in Y ) iff contradiction ) by A2, TARSKI:def 3;
hence ( x in X \ Y iff x in {} ) by XBOOLE_0:def 5; :: thesis: verum

end;

hence X \ Y = {} by TARSKI:1; :: thesis: verum