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 = {}

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 {} )

hence
X \ Y = {}
by TARSKI:2; :: thesis: verum( 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;( ( 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