let X be non emptyset ; :: 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 S1[ 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 inunion X & S1[Y] ) )
fromXFAMILY:sch 1(); defpred S2[ set ] means $1 meets X; consider Z2 being set such that A2:
for Y being set holds ( Y in Z2 iff ( Y inunion(union X) & S2[Y] ) )
fromXFAMILY:sch 1(); consider Y being set such that A3:
Y in(X \/ Z1)\/ Z2
and A4:
Y misses(X \/ Z1)\/ Z2
byTh1;