let X, Y be set ; :: thesis: X \ Y misses Y \ X
assume X \ Y meets Y \ X ; :: thesis: contradiction
then consider x being object such that
A1: x in X \ Y and
A2: x in Y \ X by XBOOLE_0:3;
x in X by A1, XBOOLE_0:def 5;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum