theorem :: ENUMSET1:86

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