let C be Category; :: thesis: Alter C is associative
thus the Comp of (Alter C) is associative by Th14; :: according to ALTCAT_1:def 15 :: thesis: verum