theorem :: PRE_POLY:44

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