let X be non empty set ; :: thesis: ( {{}} is Element of X implies not {{}} in Funcs X )
assume A1: {{}} is Element of X ; :: thesis: not {{}} in Funcs X
assume A2: {{}} in Funcs X ; :: thesis: contradiction
set FAB = { (Funcs (A,B)) where A, B is Element of X : verum } ;
reconsider x = {{}} as Element of X by A1;
consider y being set such that
A3: ( x in y & y in { (Funcs (A,B)) where A, B is Element of X : verum } ) by A2, TARSKI:def 4;
consider A, B being Element of X such that
A4: y = Funcs (A,B) by A3;
consider f being Function such that
A5: x = f and
A6: dom f = A and
A7: rng f c= B by A3, A4, FUNCT_2:def 2;
reconsider f = f as Function of A,B by A6, A7, FUNCT_2:2;
A8: {{}} = f by A5;
{} in {{}} by TARSKI:def 1;
then consider u, v being object such that
u in A and
v in B and
A9: {} = [u,v] by A8, ZFMISC_1:def 2;
thus contradiction by A9; :: thesis: verum