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

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