:: deftheorem Def12 defines with_identities CAT_6:def 12 :
for C being CategoryStr holds
( C is with_identities iff ( C is with_left_identities & C is with_right_identities ) );