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

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