let X be non empty set ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2 being set st Y1 in Y2 & Y2 in Y holds
Y1 misses X ) )
defpred S₁[ set ] means ex Y1 being set st
( Y1 in $1 & Y1 meets X );
consider Z1 being set such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S₁[Y] ) ) from XFAMILY:sch 1();
defpred S₂[ set ] means $1 meets X;
consider Z2 being set such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S₂[Y] ) ) from XFAMILY:sch 1();
consider Y being set such that
A3: Y in (X \/ Z1) \/ Z2 and
A4: Y misses (X \/ Z1) \/ Z2 by Th1;

A5: now :: thesis: not Y in Z1

assume A6: Y in Z1 ; :: thesis: contradiction
then consider Y1 being set such that
A7: Y1 in Y and
A8: Y1 meets X by A1;
Y in union X by A1, A6;
then Y1 in union (union X) by A7, TARSKI:def 4;
then Y1 in Z2 by A2, A8;
then Y1 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum

end;

assume A9: for Y being set holds
( not Y in X or ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in Y & not Y1 misses X ) ) ; :: thesis: contradiction

A10: now :: thesis: not Y in X

assume A11: Y in X ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A12: Y1 in Y2 and
A13: Y2 in Y and
A14: not Y1 misses X by A9;
Y2 in union X by A11, A13, TARSKI:def 4;
then Y2 in Z1 by A1, A12, A14;
then Y2 in X \/ Z1 by XBOOLE_0:def 3;
then Y2 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
hence contradiction by A4, A13, XBOOLE_0:3; :: thesis: verum

end;

Y in X \/ (Z1 \/ Z2) by A3, XBOOLE_1:4;
then Y in Z1 \/ Z2 by A10, XBOOLE_0:def 3;
then Y in Z2 by A5, XBOOLE_0:def 3;
then Y meets X by A2;
then Y meets X \/ Z1 by XBOOLE_1:70;
hence contradiction by A4, XBOOLE_1:70; :: thesis: verum