let C be non empty with_units AltCatStr ; :: thesis: for o being object of C holds idm o in <^o,o^>
let o be object of C; :: thesis: idm o in <^o,o^>
<^o,o^> <> {} by Th21;
hence idm o in <^o,o^> ; :: thesis: verum