theorem :: ZFMISC_1:23
for x, y being object st x <> y holds
{x} \+\ {y} = {x,y}