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 Th15; :: according to ALTCAT_1:def 16 :: thesis: verum