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