defpred S_{1}[ 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_{1}[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

( 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

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