let C be Category; :: thesis: Alter C is with_units
thus ( the Comp of (Alter C) is with_left_units & the Comp of (Alter C) is with_right_units ) by Th16; :: according to ALTCAT_1:def 18 :: thesis: verum