let C1, C2, C3 be AltCatStr ; :: thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3 )
assume ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the Comp of C3 ) ; :: according to ALTCAT_2:def 11 :: thesis: C1 is SubCatStr of C3
hence ( the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the Arrows of C3 & the Comp of C1 cc= the Comp of C3 ) by Th8; :: according to ALTCAT_2:def 11 :: thesis: verum