theorem Th30: :: BAGORDER:33

for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT)