set X = { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } ;

set Y = { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] } ;

A2: { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] } c= { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }
_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } c= { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] }
_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } = { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] }
by A2; :: thesis: verum

set Y = { F

A2: { F

proof

{ F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] } or x in { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } )

assume x in { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] }
; :: thesis: x in { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }

then consider v1 being Element of F_{1}() such that

A3: x = F_{3}(v1)
and

A4: P_{1}[v1]
;

x = F_{2}(v1)
by A1, A3;

hence x in { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }
by A4; :: thesis: verum

end;assume x in { F

then consider v1 being Element of F

A3: x = F

A4: P

x = F

hence x in { F

proof

hence
{ F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] } or x in { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] } )

assume x in { F_{2}(v1) where v1 is Element of F_{1}() : P_{1}[v1] }
; :: thesis: x in { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] }

then consider v1 being Element of F_{1}() such that

A5: x = F_{2}(v1)
and

A6: P_{1}[v1]
;

x = F_{3}(v1)
by A1, A5;

hence x in { F_{3}(v2) where v2 is Element of F_{1}() : P_{1}[v2] }
by A6; :: thesis: verum

end;assume x in { F

then consider v1 being Element of F

A5: x = F

A6: P

x = F

hence x in { F