let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition implies Intersect A,B is SubCatStr of A )
set AB = Intersect A,B;
assume A1: A,B have_the_same_composition ; :: thesis: Intersect A,B is SubCatStr of A
then A2: the Comp of (Intersect A,B) = Intersect the Comp of A,the Comp of B by Def3;
( the carrier of (Intersect A,B) = the carrier of A /\ the carrier of B & the Arrows of (Intersect A,B) = Intersect the Arrows of A,the Arrows of B ) by A1, Def3;
hence ( the carrier of (Intersect A,B) c= the carrier of A & the Arrows of (Intersect A,B) cc= the Arrows of A & the Comp of (Intersect A,B) cc= the Comp of A ) by A2, Th15, XBOOLE_1:17; :: according to ALTCAT_2:def 11 :: thesis: verum