let C be AltCatStr ; :: thesis: C is SubCatStr of C
thus the carrier of C c= the carrier of C ; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C )
thus ( the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C ) ; :: thesis: verum