let C be AltGraph ; for o being Object of C holds
( o is initial iff for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
let o be Object of C; ( o is initial iff for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
thus
( o is initial implies for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
( ( for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) ) implies o is initial )proof
assume A1:
o is
initial
;
for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) )
let o1 be
Object of
C;
ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) )
consider M being
Morphism of
o,
o1 such that A2:
M in <^o,o1^>
and A3:
<^o,o1^> is
trivial
by A1;
ex
i being
object st
<^o,o1^> = {i}
by A2, A3, ZFMISC_1:131;
then
<^o,o1^> = {M}
by TARSKI:def 1;
then
for
M1 being
Morphism of
o,
o1 st
M1 in <^o,o1^> holds
M = M1
by TARSKI:def 1;
hence
ex
M being
Morphism of
o,
o1 st
(
M in <^o,o1^> & ( for
M1 being
Morphism of
o,
o1 st
M1 in <^o,o1^> holds
M = M1 ) )
by A2;
verum
end;
assume A4:
for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) )
; o is initial
let o1 be Object of C; ALTCAT_3:def 9 ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial )
consider M being Morphism of o,o1 such that
A5:
M in <^o,o1^>
and
A6:
for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1
by A4;
A7:
<^o,o1^> c= {M}
{M} c= <^o,o1^>
by A5, TARSKI:def 1;
then
<^o,o1^> = {M}
by A7, XBOOLE_0:def 10;
hence
ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial )
; verum