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;

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

end;now :: thesis: contradiction

hence
contradiction
; :: thesis: verumconsider 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;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

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

hence
ex x being set st a = {x}
; :: thesis: verumassume
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;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