defpred S₁[ set ] means not $1 in Y;
thus ex Z being set st
for x being set holds
( x in Z iff ( x in X & S₁[x] ) ) from XBOOLE_0:sch 1(); :: thesis: verum