let C1, C2 be AltCatStr ; :: thesis: ( C1 is SubCatStr of C2 & C2 is SubCatStr of C1 implies AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
assume that
A1: ( the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 ) and
A2: the Comp of C1 cc= the Comp of C2 and
A3: ( the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the Arrows of C1 ) and
A4: the Comp of C2 cc= the Comp of C1 ; :: according to ALTCAT_2:def 11 :: thesis: AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
( the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of C2 ) by A1, A3, Th7, XBOOLE_0:def 10;
hence AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) by A2, A4, Th7; :: thesis: verum