:: deftheorem defines id- CAT_6:def 20 :
for C being with_identities CategoryStr
for o being Object of C holds id- o = o;