theorem :: ZFMISC_1:10

for x, y being object st {x} misses {y} holds
x <> y ;