assume
{ F_{3}(y) where y is Element of F_{1}() : ( P_{1}[y] & not F_{3}(y) in F_{2}() ) } meets F_{2}()
; :: thesis: contradiction

then consider x being object such that

A1: x in { F_{3}(y) where y is Element of F_{1}() : ( P_{1}[y] & not F_{3}(y) in F_{2}() ) }
and

A2: x in F_{2}()
by XBOOLE_0:3;

ex y being Element of F_{1}() st

( x = F_{3}(y) & P_{1}[y] & not F_{3}(y) in F_{2}() )
by A1;

hence contradiction by A2; :: thesis: verum

then consider x being object such that

A1: x in { F

A2: x in F

ex y being Element of F

( x = F

hence contradiction by A2; :: thesis: verum