theorem Th15: :: ALTCAT_2:15

for C being Category holds
( the_comps_of C is with_left_units & the_comps_of C is with_right_units )