let X be non empty set ; :: thesis: ex Y being set st
( Y in X & Y misses X )
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
consider Y being set such that
A2: Y in X and
A3: for x being object holds
( not x in X or not x in Y ) by A1, TARSKI:3;
take Y ; :: thesis: ( Y in X & Y misses X )
for x being object holds
( not x in X or not x in Y ) by A3;
hence ( Y in X & Y misses X ) by A2, XBOOLE_0:3; :: thesis: verum