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 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 Intersect A,B = Intersect B,A by A1, A2, Def3; :: thesis: verum