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 ;
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 ;
reconsider fy = (@ a) --> y as Function of (@ a),(@ a) by ;
reconsider fx = (@ a) --> the Element of @ a as Function of (@ a),(@ a) by ;
fx . y = the Element of @ a by ;
then A9: fx <> fy by ;
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 ;
A12: m2 in Hom (a,a) by ;
m1 in Hom (a,a) by ;
then reconsider f = @ m1, g = @ m2 as Morphism of a,a by ;
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