theorem :: PRE_POLY:82

for n being Ordinal
for b being bag of n holds RelIncl n linearly_orders support b