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]
byA1; thus { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F2(v2) where v2 is Element of F1() : P2[v2] } fromFRAENKEL: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]
byA1; thus { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } fromFRAENKEL:sch 1(A3);:: thesis: verum