theorem Th12: :: CAT_7:12

for C, D being composable with_identities CategoryStr holds
( C ~= D iff ex F being Functor of C,D st
( F is covariant & F is bijective ) )