let Y, X be set ; :: thesis: ( ( X \+\ Y = {} implies X = Y ) & ( X = Y implies X \+\ Y = {} ) & ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds
( {x} \ Y = {} iff x in Y ) ) )
set Z = X \+\ Y;
set Z1 = X \ Y;
set Z2 = Y \ X;
thus ( X \+\ Y = {} implies X = Y ) :: thesis: ( ( X = Y implies X \+\ Y = {} ) & ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds
( {x} \ Y = {} iff x in Y ) ) )

proof

assume X \+\ Y = {} ; :: thesis: X = Y
then ( X \ Y = {} & Y \ X = {} ) ;
then ( X c= Y & Y c= X ) by XBOOLE_1:37;
hence X = Y ; :: thesis: verum

end;

thus ( X = Y implies X \+\ Y = {} ) ; :: thesis: ( ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds
( {x} \ Y = {} iff x in Y ) ) )
thus ( X \ Y = {} iff X c= Y ) by XBOOLE_1:37; :: thesis: for x being object holds
( {x} \ Y = {} iff x in Y )
thus for x being object holds
( {x} \ Y = {} iff x in Y ) by ZFMISC_1:60; :: thesis: verum