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 A,B have_the_same_composition ; :: thesis: Intersect A,B is SubCatStr of A
then ( 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 & the Comp of (Intersect A,B) = Intersect the Comp of A,the Comp of B ) by 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 Th15, XBOOLE_1:17; :: according to ALTCAT_2:def 11 :: thesis: verum