:: deftheorem Def3 defines Intersect YELLOW20:def 3 :
for A, B being AltCatStr st A,B have_the_same_composition holds
for b₃ being strict AltCatStr holds
( b₃ = Intersect (A,B) iff ( the carrier of b₃ = the carrier of A /\ the carrier of B & the Arrows of b₃ = Intersect ( the Arrows of A, the Arrows of B) & the Comp of b₃ = Intersect ( the Comp of A, the Comp of B) ) );