theorem Th1: :: FACIRC_2:1

for x, y, z being set st x <> z & y <> z holds
{x,y} \ {z} = {x,y}