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