let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{1}[s,t] } or x in { F_{3}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{2}[s1,t1] } )

assume x in { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : P_{1}[s,t] }
; :: thesis: x in { F_{3}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{2}[s1,t1] }

then consider s being Element of F_{1}(), t being Element of F_{2}() such that

A2: x = F_{3}(s,t)
and

A3: P_{1}[s,t]
;

ex s9 being Element of F_{1}() st

( P_{2}[s9,t] & F_{3}(s,t) = F_{3}(s9,t) )
by A1, A3;

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

assume x in { F

then consider s being Element of F

A2: x = F

A3: P

ex s9 being Element of F

( P

hence x in { F