let X be set ; :: thesis: ( X <> {} implies ex Y being set st
( Y in X & Y misses X ) )
set x = the Element of X;
assume X <> {} ; :: thesis: ex Y being set st
( Y in X & Y misses X )
then the Element of X in X ;
then 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;
take Y ; :: thesis: ( Y in X & Y misses X )
thus ( Y in X & Y misses X ) by A1, XBOOLE_0:3; :: thesis: verum