let X be set ; :: thesis: ( X <> {} implies ex Y being set st
( Y in X & ( for Y1 being set st Y1 in Y holds
Y1 misses X ) ) )
defpred S₁[ set ] means $1 meets X;
consider Z being set such that
A1: for Y being set holds
( Y in Z iff ( Y in union X & S₁[Y] ) ) from XBOOLE_0:sch 1();
assume X <> {} ; :: thesis: ex Y being set st
( Y in X & ( for Y1 being set st Y1 in Y holds
Y1 misses X ) )
then consider Y being set such that
A2: Y in X \/ Z and
A3: Y misses X \/ Z by Th1;
assume A4: for Y being set holds
( not Y in X or ex Y1 being set st
( Y1 in Y & not Y1 misses X ) ) ; :: thesis: contradiction

now

assume A5: Y in X ; :: thesis: contradiction
then consider Y1 being set such that
A6: Y1 in Y and
A7: not Y1 misses X by A4;
Y1 in union X by A5, A6, TARSKI:def 4;
then Y1 in Z by A1, A7;
then Y1 in X \/ Z by XBOOLE_0:def 3;
hence contradiction by A3, A6, XBOOLE_0:3; :: thesis: verum

end;

then Y in Z by A2, XBOOLE_0:def 3;
then Y meets X by A1;
hence contradiction by A3, XBOOLE_1:70; :: thesis: verum