let x, y be object ; for X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
let X, Y be set ; ( x <> y implies ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) )
assume
x <> y
; ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
then
{x} misses {y}
by Th11;
hence
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
by Th103; verum