let X be non empty set ; ex Y being set st
( Y in X & ( for Y1, Y2, Y3 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds
Y1 misses X ) )
defpred S1[ set ] means ex Y1, Y2 being set st
( Y1 in Y2 & Y2 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 );
consider Z2 being set such that
A2:
for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S3[Y] ) )
from XFAMILY:sch 1();
consider Z3 being set such that
A3:
for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S2[Y] ) )
from XFAMILY:sch 1();
consider Y being set such that
A4:
Y in ((X \/ Z1) \/ Z2) \/ Z3
and
A5:
Y misses ((X \/ Z1) \/ Z2) \/ Z3
by Th1;
set V = ((X \/ Z1) \/ Z2) \/ Z3;
A15: ((X \/ Z1) \/ Z2) \/ Z3 =
(X \/ (Z1 \/ Z2)) \/ Z3
by XBOOLE_1:4
.=
X \/ ((Z1 \/ Z2) \/ Z3)
by XBOOLE_1:4
;
assume A16:
for Y being set holds
( not Y in X or ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X ) )
; contradiction
then
Y in (Z1 \/ Z2) \/ Z3
by A15, A4, XBOOLE_0:def 3;
then
Y in Z1 \/ (Z2 \/ Z3)
by XBOOLE_1:4;
then
Y in Z2 \/ Z3
by A10, XBOOLE_0:def 3;
then
Y in Z3
by A6, XBOOLE_0:def 3;
then
Y meets X
by A3;
hence
contradiction
by A15, A5, XBOOLE_1:70; verum