consider x being object such that
A1: x in X by XBOOLE_0:def 1;
reconsider x = x as Element of X by A1;
consider y being object such that
A2: y in Y by XBOOLE_0:def 1;
reconsider y = y as Element of Y by A2;
x \ y in DIFFERENCE (X,Y) by SETFAM_1:def 6;
hence not DIFFERENCE (X,Y) is empty ; :: thesis: verum