let Y, X be set ; :: thesis: ( X \+\ Y = {} iff X = 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 = {} )

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 by XBOOLE_0:def 10; :: thesis: verum

end;

assume X = Y ; :: thesis: X \+\ Y = {}
hence X \+\ Y = {} ; :: thesis: verum