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}
consider x being Element of @ a;

A3: now

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

now

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

end;

hence contradiction ; :: thesis: verum

end;

now

assume a <> {x} ; :: thesis: contradiction
then consider y being set such that
A7: y in @ a and
A8: y <> x by A3, ZFMISC_1:41;
reconsider fy = (@ a) --> y as Function of (@ a),(@ a) by A7, FUNCOP_1:57;
reconsider fx = (@ a) --> x as Function of (@ a),(@ a) by A7, FUNCOP_1:57;
fx . y = x by A7, FUNCOP_1:13;
then A9: fx <> fy by A7, A8, FUNCOP_1:13;
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, Th27;
m1 in Hom (a,a) by A10, Th27;
then reconsider f = @ m1, g = @ m2 as Morphism of a,a by A12, CAT_1:def 7;
consider h being Morphism of a,a such that
A13: for h9 being Morphism of a,a holds h = h9 by A2, CAT_1:def 15;
f = h by A13
.= g by A13 ;
hence contradiction by A9, ZFMISC_1:33; :: thesis: verum

end;

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