set Y = { F_{4}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{1}[u2,v2] } ;

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

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

set X = { F

A2: { F

proof

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

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

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

A3: x = F_{4}(u1,v1)
and

A4: P_{1}[u1,v1]
;

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

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

end;assume x in { F

then consider u1 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_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } or x in { F_{4}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{1}[u2,v2] } )

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

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

A5: x = F_{3}(u1,v1)
and

A6: P_{1}[u1,v1]
;

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

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

end;assume x in { F

then consider u1 being Element of F

A5: x = F

A6: P

x = F

hence x in { F