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_{3}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{2}[u2,v2] } )

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

then consider u being Element of F_{1}(), v being Element of F_{2}() such that

A2: x = F_{3}(u,v)
and

A3: P_{1}[u,v]
;

P_{2}[u,v]
by A1, A3;

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

assume x in { F

then consider u being Element of F

A2: x = F

A3: P

P

hence x in { F