theorem Th41: :: PRE_POLY:42

for n being Ordinal
for p, q, r being bag of n st p <=' q & q <=' r holds
p <=' r by Th40;