for i, j being Nat
for b being bag of j st i <= j holds
b | i is Element of Bags i