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 Th12;
hence idm o in <^o,o^> ; :: thesis: verum