theorem Th17: :: ALTCAT_2:17

for C being Category holds Alter C is with_units