let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } or x in { F₃(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₂[u2,v2] } )
assume x in { F₃(u9,v9) where u9 is Element of F₁(), v9 is Element of F₂() : P₁[u9,v9] } ; :: thesis: x in { F₃(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₂[u2,v2] }
then consider u being Element of F₁(), v being Element of F₂() such that
A2: x = F₃(u,v) and
A3: P₁[u,v] ;
P₂[u,v] by A1, A3;
hence x in { F₃(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₂[u2,v2] } by A2; :: thesis: verum