theorem Th14: :: HILB10_2:14

for k, n being Nat
for b1, b2 being bag of n holds
( b1 < b2 iff b1 bag_extend k < b2 bag_extend k )