set e = the Element of F1();
set LH = { F2(x) where x is Element of F1() : P1[x,F1()] } ;
set RH = {F2( the Element of F1())};
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { F2(x) where x is Element of F1() : P1[x,F1()] } or z in {F2( the Element of F1())} )
assume z in { F2(x) where x is Element of F1() : P1[x,F1()] } ; :: thesis: z in {F2( the Element of F1())}
then consider x being Element of F1() such that
A1: ( z = F2(x) & P1[x,F1()] ) ;
x \+\ the Element of F1() = {} ;
then z = F2( the Element of F1()) by A1, Th29;
hence z in {F2( the Element of F1())} by TARSKI:def 1; :: thesis: verum