let C be AltGraph ; :: thesis: for o being Object of C holds
( o is terminal iff for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
let o be Object of C; :: thesis: ( o is terminal iff for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
thus ( o is terminal implies for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ) :: thesis: ( ( for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ) implies o is terminal )

proof

assume A1: o is terminal ; :: thesis: for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) )
let o1 be Object of C; :: thesis: ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) )
consider M being Morphism of o1,o such that
A2: M in <^o1,o^> and
A3: <^o1,o^> is trivial by A1;
ex i being object st <^o1,o^> = {i} by A2, A3, ZFMISC_1:131;
then <^o1,o^> = {M} by TARSKI:def 1;
then for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 by TARSKI:def 1;
hence ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) by A2; :: thesis: verum

end;

assume A4: for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) ; :: thesis: o is terminal
let o1 be Object of C; :: according to ALTCAT_3:def 10 :: thesis: ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial )
consider M being Morphism of o1,o such that
A5: M in <^o1,o^> and
A6: for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 by A4;
A7: <^o1,o^> c= {M}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <^o1,o^> or x in {M} )
assume A8: x in <^o1,o^> ; :: thesis: x in {M}
then reconsider M1 = x as Morphism of o1,o ;
M1 = M by A6, A8;
hence x in {M} by TARSKI:def 1; :: thesis: verum

end;

{M} c= <^o1,o^> by A5, TARSKI:def 1;
then <^o1,o^> = {M} by A7, XBOOLE_0:def 10;
hence ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial ) ; :: thesis: verum