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

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