let X be non empty set ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds
Y1 misses X ) )
defpred S₁[ set ] means ex Y1, Y2, Y3, Y4 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 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;
defpred S₃[ set ] means ex Y1 being set st
( Y1 in $1 & Y1 meets X );
defpred S₄[ set ] means ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in $1 & Y1 meets X );
defpred S₅[ set ] means ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 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 Z5 being set such that
A3: for Y being set holds
( Y in Z5 iff ( Y in union (union (union (union (union X)))) & S₂[Y] ) ) from XFAMILY:sch 1();
consider Z3 being set such that
A4: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S₄[Y] ) ) from XFAMILY:sch 1();
consider Z4 being set such that
A5: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S₃[Y] ) ) from XFAMILY:sch 1();
set V = ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5;
consider Y being set such that
A6: Y in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 and
A7: Y misses ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by Th1;
A8: ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 = (((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_1:4
.= ((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5 by XBOOLE_1:4
.= (X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5 by XBOOLE_1:4
.= X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) by XBOOLE_1:4 ;

A9: now :: thesis: not Y in Z1

assume A10: Y in Z1 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set such that
A11: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A12: Y4 in Y and
A13: Y1 meets X by A1;
Y in union X by A1, A10;
then Y4 in union (union X) by A12, TARSKI:def 4;
then Y4 in Z2 by A2, A11, A13;
then Y4 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y meets (X \/ Z1) \/ Z2 by A12, XBOOLE_0:3;
then Y meets ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_1:70;
then Y meets (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_1:70;
hence contradiction by A7, XBOOLE_1:70; :: thesis: verum

end;

A14: now :: thesis: not Y in Z2

assume A15: Y in Z2 ; :: thesis: contradiction
then consider Y1, Y2, Y3 being set such that
A16: ( Y1 in Y2 & Y2 in Y3 ) and
A17: Y3 in Y and
A18: Y1 meets X by A2;
Y in union (union X) by A2, A15;
then Y3 in union (union (union X)) by A17, TARSKI:def 4;
then Y3 in Z3 by A4, A16, A18;
then Y3 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y3 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y3 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
hence contradiction by A7, A17, XBOOLE_0:3; :: thesis: verum

end;

A19: now :: thesis: not Y in Z3

assume A20: Y in Z3 ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A21: Y1 in Y2 and
A22: Y2 in Y and
A23: Y1 meets X by A4;
Y in union (union (union X)) by A4, A20;
then Y2 in union (union (union (union X))) by A22, TARSKI:def 4;
then Y2 in Z4 by A5, A21, A23;
then Y2 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y2 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
hence contradiction by A7, A22, XBOOLE_0:3; :: thesis: verum

end;

A24: now :: thesis: not Y in Z4

assume A25: Y in Z4 ; :: thesis: contradiction
then consider Y1 being set such that
A26: Y1 in Y and
A27: Y1 meets X by A5;
Y in union (union (union (union X))) by A5, A25;
then Y1 in union (union (union (union (union X)))) by A26, TARSKI:def 4;
then Y1 in Z5 by A3, A27;
then Y1 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
hence contradiction by A7, A26, XBOOLE_0:3; :: thesis: verum

end;

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

now :: thesis: not Y in X

assume A29: Y in X ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5 being set such that
A30: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 ) and
A31: Y5 in Y and
A32: not Y1 misses X by A28;
Y5 in union X by A29, A31, TARSKI:def 4;
then Y5 in Z1 by A1, A30, A32;
then Y5 in X \/ Z1 by XBOOLE_0:def 3;
then Y5 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y5 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y meets ((X \/ Z1) \/ Z2) \/ Z3 by A31, XBOOLE_0:3;
then Y meets (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_1:70;
hence contradiction by A7, XBOOLE_1:70; :: thesis: verum

end;

then Y in (((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5 by A8, A6, XBOOLE_0:def 3;
then Y in ((Z1 \/ (Z2 \/ Z3)) \/ Z4) \/ Z5 by XBOOLE_1:4;
then Y in (Z1 \/ ((Z2 \/ Z3) \/ Z4)) \/ Z5 by XBOOLE_1:4;
then Y in Z1 \/ (((Z2 \/ Z3) \/ Z4) \/ Z5) by XBOOLE_1:4;
then Y in ((Z2 \/ Z3) \/ Z4) \/ Z5 by A9, XBOOLE_0:def 3;
then Y in (Z2 \/ (Z3 \/ Z4)) \/ Z5 by XBOOLE_1:4;
then Y in Z2 \/ ((Z3 \/ Z4) \/ Z5) by XBOOLE_1:4;
then Y in (Z3 \/ Z4) \/ Z5 by A14, XBOOLE_0:def 3;
then Y in Z3 \/ (Z4 \/ Z5) by XBOOLE_1:4;
then Y in Z4 \/ Z5 by A19, XBOOLE_0:def 3;
then Y in Z5 by A24, XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A8, A7, XBOOLE_1:70; :: thesis: verum