let C be non empty with_units AltCatStr ; :: thesis: for o being object of C holds <^o,o^> <> {}
let o be object of C; :: thesis: <^o,o^> <> {}
the Comp of C is with_left_units by Def18;
then ex e being set st
( e in the Arrows of C . o,o & ( for o9 being Element of C
for f being set st f in the Arrows of C . o9,o holds
(the Comp of C . o9,o,o) . e,f = f ) ) by Def9;
hence <^o,o^> <> {} ; :: thesis: verum