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

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

A2: for u being Element of F_{1}()

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

P_{2}[u,v]
by A1;

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

A3: for u being Element of F_{1}()

for v being Element of F_{2}() st P_{2}[u,v] holds

P_{1}[u,v]
by A1;

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

set A = { F

A2: for u being Element of F

for v being Element of F

P

thus { F

A3: for u being Element of F

for v being Element of F

P

thus { F