set B = { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } ;
set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ;
A2: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
P2[u,v] by A1;
thus { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } c= { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } from FRAENKEL:sch 2(A2); :: according to XBOOLE_0:def 10 :: thesis: { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } c= { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
A3: for u being Element of F1()
for v being Element of F2() st P2[u,v] holds
P1[u,v] by A1;
thus { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } c= { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } from FRAENKEL:sch 2(A3); :: thesis: verum