theorem Th15: :: BAGORDER:16

for i, j, n being Nat holds (i,j) -cut (EmptyBag n) = EmptyBag (j -' i)