theorem NF501: :: BINPACK1:3

for x, y being object holds {[x,y]} " {y} = {x}