set X = { F2(v1) where v1 is Element of F1() : P1[v1] } ;
set Y = { F3(v2) where v2 is Element of F1() : P1[v2] } ;
A2: { F3(v2) where v2 is Element of F1() : P1[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(v2) where v2 is Element of F1() : P1[v2] } or x in { F2(v1) where v1 is Element of F1() : P1[v1] } )
assume x in { F3(v2) where v2 is Element of F1() : P1[v2] } ; :: thesis: x in { F2(v1) where v1 is Element of F1() : P1[v1] }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
 x = F2(v1) by A1, A3, A4;
hence x in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; :: thesis: verum
end;
{ F2(v1) where v1 is Element of F1() : P1[v1] } c= { F3(v2) where v2 is Element of F1() : P1[v2] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F2(v1) where v1 is Element of F1() : P1[v1] } or x in { F3(v2) where v2 is Element of F1() : P1[v2] } )
assume x in { F2(v1) where v1 is Element of F1() : P1[v1] } ; :: thesis: x in { F3(v2) where v2 is Element of F1() : P1[v2] }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
 x = F3(v1) by A1, A5, A6;
hence x in { F3(v2) where v2 is Element of F1() : P1[v2] } by A6; :: thesis: verum
end;
hence { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } by A2; :: thesis: verum