set A = { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } ;

set B = { F_{2}(v2) where v2 is Element of F_{1}() : P_{2}[v2] } ;

A2: for v being Element of F_{1}() st P_{1}[v] holds

P_{2}[v]
by A1;

thus { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } c= { F_{2}(v2) where v2 is Element of F_{1}() : P_{2}[v2] }
from FRAENKEL:sch 1(A2); :: according to XBOOLE_0:def 10 :: thesis: { F_{2}(v2) where v2 is Element of F_{1}() : P_{2}[v2] } c= { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }

A3: for v being Element of F_{1}() st P_{2}[v] holds

P_{1}[v]
by A1;

thus { F_{2}(v2) where v2 is Element of F_{1}() : P_{2}[v2] } c= { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }
from FRAENKEL:sch 1(A3); :: thesis: verum

set B = { F

A2: for v being Element of F

P

thus { F

A3: for v being Element of F

P

thus { F