theorem Th1: :: ORDERS_5:1

for A, B being set
for x being object st A = B \ {x} & x in B holds
B \ A = {x}