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