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 consider e being set such that
A1: e in the Arrows of C . o,o and
for o' being Element of C
for f being set st f in the Arrows of C . o',o holds
(the Comp of C . o',o,o) . e,f = f by Def9;
thus <^o,o^> <> {} by A1; :: thesis: verum