theorem :: CAT_6:20

for C being CategoryStr holds
( C is with_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_identities ) by Th17, Th19;