let x, y be object ; :: thesis: for X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )
let 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 Th11;
hence ( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] ) by Th103; :: thesis: verum