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}

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 <> {} & @ C <> {} ) by A2, A6, CAT_1:def 15;
then ( Funcs (@ (@ C)),(@ a) <> {} & @ (@ C) <> {} ) by Lm6;
hence contradiction by A4; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

consider x being Element of @ a;

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 fx = (@ a) --> x as Function of (@ a),(@ a) by A7, FUNCOP_1:57;
reconsider fy = (@ a) --> y as Function of (@ a),(@ a) by A7, FUNCOP_1:57;
A9: ( [[(@ a),(@ a)],fx] in Maps (@ a),(@ a) & [[(@ 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 A9;
( m1 in Hom a,a & m2 in Hom a,a ) by A9, Th27;
then reconsider f = @ m1, g = @ m2 as Morphism of a,a by CAT_1:def 7;
consider h being Morphism of a,a such that
A10: for h' being Morphism of a,a holds h = h' by A2, CAT_1:def 15;

now

thus f = h by A10
.= g by A10 ; :: thesis: ( f = [[(@ a),(@ a)],fx] & g = [[(@ a),(@ a)],fy] & fx <> fy )
thus ( f = [[(@ a),(@ a)],fx] & g = [[(@ a),(@ a)],fy] ) ; :: thesis: fx <> fy
( fx . y = x & fy . y = y ) by A7, FUNCOP_1:13;
hence fx <> fy by A8; :: thesis: verum

end;

hence contradiction by ZFMISC_1:33; :: thesis: verum

end;

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