theorem Th21: :: YELLOW20:21

for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being Object of A
for b1, b2 being Object of B
for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>