theorem :: YELLOW20:24

for A, B being non empty with_units AltCatStr st A,B have_the_same_composition holds
for a being Object of A
for b being Object of B
for o being Object of (Intersect (A,B)) st o = a & o = b & idm a = idm b holds
idm a in <^o,o^> by Th23;