theorem :: ZFMISC_1:17

for x, y being object st x <> y holds
{x,y} \ {y} = {x}