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

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

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

A2: x = F_{2}(v)
and

A3: P_{1}[v]
;

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

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

assume x in { F

then consider v being Element of F

A2: x = F

A3: P

P

hence x in { F