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