let V be non empty set ; 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); ( V <> {{}} & a is terminal implies ex x being set st a = {x} )
assume that
A1:
V <> {{}}
and
A2:
a is terminal
; ex x being set st a = {x}
set x = the Element of @ a;
A3:
now not @ a = {} assume A4:
@ a = {}
;
contradictionhence
contradiction
;
verum end;
now not a <> { the Element of @ a}assume
a <> { the Element of @ a}
;
contradictionthen 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;
verum end;
hence
ex x being set st a = {x}
; verum