let C be non empty transitive AltCatStr ; :: thesis: for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
let D be SubCatStr of C; :: thesis: ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )
assume that
A1: the carrier of D = the carrier of C and
A2: the Arrows of D = the Arrows of C ; :: thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
A3: D is transitive

proof

let o1, o2, o3 be Object of D; :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1;
assume A4: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}
A5: <^o1,o3^> = <^p1,p3^> by A2;
( <^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> ) by A2;
hence not <^o1,o3^> = {} by A5, A4, ALTCAT_1:def 2; :: thesis: verum

end;

A6: C is SubCatStr of C by Th20;
not D is empty by A1;
then C is SubCatStr of D by A1, A2, A3, A6, Th24;
hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Th22; :: thesis: verum