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

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