theorem Th9: :: POLYALGX:9

for n being Ordinal holds BagOrder n linearly_orders Bags n