defpred S₁[ set ] means ex y being Element of Elements N st
( y in X & $1 = enter (N,y) );
consider F being Subset-Family of (Elements N) such that
A1: for x being Subset of (Elements N) holds
( x in F iff S₁[x] ) from SUBSET_1:sch 3();
take F ; :: thesis: for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) )
thus for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) by A1; :: thesis: verum