let V be non empty set ; :: thesis: for a being Object of (Ens V) st V <> {{}} & a is terminal holds
ex x being set st a = {x}
let a be Object of (Ens V); :: thesis: ( V <> {{}} & a is terminal implies ex x being set st a = {x} )
assume that
A1: V <> {{}} and
A2: a is terminal ; :: thesis: ex x being set st a = {x}
set x = the Element of @ a;

A3: now :: thesis: not @ a = {}

assume A4: @ a = {} ; :: thesis: contradiction

now :: thesis: contradiction

consider C being object such that
A5: C in V and
A6: C <> {} by A1, ZFMISC_1:35;
reconsider C = C as Element of V by A5;
set b = @ C;
Hom ((@ C),a) <> {} by A2;
then Funcs ((@ (@ C)),(@ a)) <> {} by Lm6;
hence contradiction by A4, A6; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

now :: thesis: not a <> { the Element of @ a}

assume a <> { the Element of @ a} ; :: thesis: contradiction
then consider y being object such that
A7: y in @ a and
A8: y <> the Element of @ a by A3, ZFMISC_1:35;
reconsider fy = (@ a) --> y as Function of (@ a),(@ a) by A7, FUNCOP_1:45;
reconsider fx = (@ a) --> the Element of @ a as Function of (@ a),(@ a) by A7, FUNCOP_1:45;
fx . y = the Element of @ a by A7, FUNCOP_1:7;
then A9: fx <> fy by A7, A8, FUNCOP_1:7;
A10: [[(@ a),(@ a)],fx] in Maps ((@ a),(@ a)) by Th15;
A11: [[(@ a),(@ a)],fy] in Maps ((@ a),(@ a)) by Th15;
Maps ((@ a),(@ a)) c= Maps V by Th17;
then reconsider m1 = [[(@ a),(@ a)],fx], m2 = [[(@ a),(@ a)],fy] as Element of Maps V by A10, A11;
A12: m2 in Hom (a,a) by A11, Th26;
m1 in Hom (a,a) by A10, Th26;
then reconsider f = @ m1, g = @ m2 as Morphism of a,a by A12, CAT_1:def 5;
consider h being Morphism of a,a such that
A13: for h9 being Morphism of a,a holds h = h9 by A2;
f = h by A13
.= g by A13 ;
hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

hence ex x being set st a = {x} ; :: thesis: verum