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

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