let X be non empty set ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds
Y1 misses X ) )
defpred S1[ set ] means ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 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 & S1[Y] ) ) from XFAMILY:sch 1();
 defpred S2[ set ] means $1 meets X;
defpred S3[ set ] means ex Y1 being set st
( Y1 in $1 & Y1 meets X );
defpred S4[ set ] means ex Y1, Y2 being set st
( Y1 in Y2 & Y2 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) & S4[Y] ) ) from XFAMILY:sch 1();
 consider Z4 being set such that
A3: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S2[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)) & S3[Y] ) ) from XFAMILY:sch 1();
 consider Y being set such that
A5: Y in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 and
A6: Y misses (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by Th1;
A7: now :: thesis: not Y in Z3
assume A8: Y in Z3 ; :: thesis: contradiction
then consider Y1 being set such that
A9: Y1 in Y and
A10: Y1 meets X by A4;
Y in union (union (union X)) by A4, A8;
then Y1 in union (union (union (union X))) by A9, TARSKI:def 4;
then Y1 in Z4 by A3, A10;
then Y1 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
hence contradiction by A6, A9, XBOOLE_0:3; :: thesis: verum
end;
A11: now :: thesis: not Y in Z1
assume A12: Y in Z1 ; :: thesis: contradiction
then consider Y1, Y2, Y3 being set such that
A13: ( Y1 in Y2 & Y2 in Y3 ) and
A14: Y3 in Y and
A15: Y1 meets X by A1;
Y in union X by A1, A12;
then Y3 in union (union X) by A14, TARSKI:def 4;
then Y3 in Z2 by A2, A13, A15;
then Y3 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y meets (X \/ Z1) \/ Z2 by A14, XBOOLE_0:3;
then Y meets ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_1:70;
hence contradiction by A6, XBOOLE_1:70; :: thesis: verum
end;
A16: (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 = ((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4 by XBOOLE_1:4
.= (X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4 by XBOOLE_1:4
.= X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4) by XBOOLE_1:4 ;
A17: now :: thesis: not Y in Z2
assume A18: Y in Z2 ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A19: Y1 in Y2 and
A20: Y2 in Y and
A21: Y1 meets X by A2;
Y in union (union X) by A2, A18;
then Y2 in union (union (union X)) by A20, TARSKI:def 4;
then Y2 in Z3 by A4, A19, A21;
then Y2 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y meets ((X \/ Z1) \/ Z2) \/ Z3 by A20, XBOOLE_0:3;
hence contradiction by A6, XBOOLE_1:70; :: thesis: verum
end;
assume A22: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & not Y1 misses X ) ) ; :: thesis: contradiction
now :: thesis: not Y in X
assume A23: Y in X ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set such that
A24: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A25: Y4 in Y and
A26: not Y1 misses X by A22;
Y4 in union X by A23, A25, TARSKI:def 4;
then Y4 in Z1 by A1, A24, A26;
then Y4 in X \/ Z1 by XBOOLE_0:def 3;
then Y4 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y4 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y4 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
hence contradiction by A6, A25, XBOOLE_0:3; :: thesis: verum
end;
then Y in ((Z1 \/ Z2) \/ Z3) \/ Z4 by A16, A5, XBOOLE_0:def 3;
then Y in (Z1 \/ (Z2 \/ Z3)) \/ Z4 by XBOOLE_1:4;
then Y in Z1 \/ ((Z2 \/ Z3) \/ Z4) by XBOOLE_1:4;
then Y in (Z2 \/ Z3) \/ Z4 by A11, XBOOLE_0:def 3;
then Y in Z2 \/ (Z3 \/ Z4) by XBOOLE_1:4;
then Y in Z3 \/ Z4 by A17, XBOOLE_0:def 3;
then Y in Z4 by A7, XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A16, A6, XBOOLE_1:70; :: thesis: verum