for n, m being Ordinal
for b being bag of n st m in n holds
b | m is bag of m