defpred S_{1}[ set ] means ( P_{2}[$1] & P_{1}[$1] );

defpred S_{2}[ set ] means ( $1 in { s1 where s1 is Element of F_{1}() : P_{2}[s1] } & P_{1}[$1] );

A1: for s being Element of F_{1}() holds

( S_{2}[s] iff S_{1}[s] )
_{2}(s) where s is Element of F_{1}() : S_{2}[s] } = { F_{2}(s2) where s2 is Element of F_{1}() : S_{1}[s2] }
from FRAENKEL:sch 3(A1); :: thesis: verum

defpred S

A1: for s being Element of F

( S

proof

thus
{ F
let s be Element of F_{1}(); :: thesis: ( S_{2}[s] iff S_{1}[s] )

_{2}[s] iff S_{1}[s] )
; :: thesis: verum

end;now :: thesis: ( s in { s1 where s1 is Element of F_{1}() : P_{2}[s1] } implies P_{2}[s] )

hence
( Sassume
s in { s1 where s1 is Element of F_{1}() : P_{2}[s1] }
; :: thesis: P_{2}[s]

then ex s1 being Element of F_{1}() st

( s = s1 & P_{2}[s1] )
;

hence P_{2}[s]
; :: thesis: verum

end;then ex s1 being Element of F

( s = s1 & P

hence P