theorem Th1: :: BAGORDER:1
for x, y, z being set st z in x & z in y & x \ {z} = y \ {z} holds
x = y