let C be non empty AltCatStr ; :: thesis: for O, A being Object of C

for M being Morphism of O,A st O is terminal holds

M is mono

let O, A be Object of C; :: thesis: for M being Morphism of O,A st O is terminal holds

M is mono

let M be Morphism of O,A; :: thesis: ( O is terminal implies M is mono )

assume A1: O is terminal ; :: thesis: M is mono

let o be Object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,O^> = {} or for b_{1}, b_{2} being M3(<^o,O^>) holds

( not M * b_{1} = M * b_{2} or b_{1} = b_{2} ) )

assume A2: <^o,O^> <> {} ; :: thesis: for b_{1}, b_{2} being M3(<^o,O^>) holds

( not M * b_{1} = M * b_{2} or b_{1} = b_{2} )

let a, b be Morphism of o,O; :: thesis: ( not M * a = M * b or a = b )

assume M * a = M * b ; :: thesis: a = b

consider N being Morphism of o,O such that

N in <^o,O^> and

A3: for M1 being Morphism of o,O st M1 in <^o,O^> holds

N = M1 by A1, ALTCAT_3:27;

thus a = N by A2, A3

.= b by A2, A3 ; :: thesis: verum

for M being Morphism of O,A st O is terminal holds

M is mono

let O, A be Object of C; :: thesis: for M being Morphism of O,A st O is terminal holds

M is mono

let M be Morphism of O,A; :: thesis: ( O is terminal implies M is mono )

assume A1: O is terminal ; :: thesis: M is mono

let o be Object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,O^> = {} or for b

( not M * b

assume A2: <^o,O^> <> {} ; :: thesis: for b

( not M * b

let a, b be Morphism of o,O; :: thesis: ( not M * a = M * b or a = b )

assume M * a = M * b ; :: thesis: a = b

consider N being Morphism of o,O such that

N in <^o,O^> and

A3: for M1 being Morphism of o,O st M1 in <^o,O^> holds

N = M1 by A1, ALTCAT_3:27;

thus a = N by A2, A3

.= b by A2, A3 ; :: thesis: verum