let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition implies Intersect A,B = Intersect B,A )
set AB = Intersect A,B;
assume A1: A,B have_the_same_composition ; :: thesis: Intersect A,B = Intersect B,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 Intersect A,B = Intersect B,A by A1, Def3; :: thesis: verum