let X be set ; :: thesis: ( X <> {} implies ex Y being set st
( Y in X & Y misses X ) )
assume A1: X <> {} ; :: thesis: ex Y being set st
( Y in X & Y misses X )
consider x being Element of X;
x in X by A1;
then consider Y being set such that
A2: ( Y in X & ( for x being set holds
( not x in X or not x in Y ) ) ) by TARSKI:7;
take Y ; :: thesis: ( Y in X & Y misses X )
thus ( Y in X & Y misses X ) by A2, XBOOLE_0:3; :: thesis: verum