theorem :: ZFMISC_1:108

for x, y being object
for X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )