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