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 set ; :: 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) & P1[V1] ) ;
P2[V1] by A1, A2;
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 set ; :: 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
A3: ( a = F2(V1) & P2[V1] ) ;
P1[V1] by A1, A3;
hence a in { F2(v1) where v1 is Element of F1() : P1[v1] } by A3; :: thesis: verum
end;