theorem Th6: :: HILBASIS:6
for n being Nat holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0