thus { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F2(v2) where v2 is Element of F1() : P2[v2] } :: 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] }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F2(v1) where v1 is Element of F1() : P1[v1] } or a in { F2(v2) where v2 is Element of F1() : P2[v2] } )
assume a in { F2(v1) where v1 is Element of F1() : P1[v1] } ; :: thesis: a in { F2(v2) where v2 is Element of F1() : P2[v2] }
then consider V1 being Element of F1() such that
A2: a = F2(V1) and
A3: P1[V1] ;
 P2[V1] by A1, A3;
hence a in { F2(v2) where v2 is Element of F1() : P2[v2] } by A2; :: thesis: verum
end;
thus { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F2(v2) where v2 is Element of F1() : P2[v2] } or a in { F2(v1) where v1 is Element of F1() : P1[v1] } )
assume a in { F2(v1) where v1 is Element of F1() : P2[v1] } ; :: thesis: a in { F2(v1) where v1 is Element of F1() : P1[v1] }
then consider V1 being Element of F1() such that
A4: a = F2(V1) and
A5: P2[V1] ;
 P1[V1] by A1, A5;
hence a in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; :: thesis: verum
end;