let x, y, X, Y be set ; :: thesis: ( x <> y implies [:X,{x}:] misses [:Y,{y}:] )
assume A1: x <> y ; :: thesis: [:X,{x}:] misses [:Y,{y}:]
assume not [:X,{x}:] misses [:Y,{y}:] ; :: thesis: contradiction
then consider z being set such that
A2: ( z in [:X,{x}:] & z in [:Y,{y}:] ) by XBOOLE_0:3;
( z `2 = x & z `2 = y ) by A2, MCART_1:13;
hence contradiction by A1; :: thesis: verum