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 ;
TARSKI:def 3 ( 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] }
;
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;
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 ;
TARSKI:def 3 ( 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] }
;
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;
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; verum