let x, y, X, Y be set ; :: thesis: ( x <> y implies ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) )
assume x <> y ; :: thesis: ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
then {x} misses {y} by Th17;
hence ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) by Th127; :: thesis: verum