let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F2(v) where v is Element of F1() : P1[v] } or x in { F2(u) where u is Element of F1() : P2[u] } )
assume x in { F2(v9) where v9 is Element of F1() : P1[v9] } ; :: thesis: x in { F2(u) where u is Element of F1() : P2[u] }
then consider v being Element of F1() such that
A2: x = F2(v) and
A3: P1[v] ;
 P2[v] by A1, A3;
hence x in { F2(u) where u is Element of F1() : P2[u] } by A2; :: thesis: verum