let C be AltGraph ; :: thesis: 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; :: thesis: ( 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 ) ) ) :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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^> & <^o,o1^> is trivial ) by A1, Def9;
consider i being set such that
A3: <^o,o1^> = {i} by A2, REALSET1:def 4;
<^o,o1^> = {M} by A3, 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; :: thesis: 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 ) ) ; :: thesis: o is initial
let o1 be object of C; :: according to ALTCAT_3:def 9 :: thesis: 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}

proof

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

end;

{M} c= <^o,o1^>

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {M} or x in <^o,o1^> )
assume x in {M} ; :: thesis: x in <^o,o1^>
hence x in <^o,o1^> by A5, TARSKI:def 1; :: thesis: verum

end;

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 ) ; :: thesis: verum