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}:] and
A3: z in [:Y,{y}:] by XBOOLE_0:3;
z `2 = x by A2, MCART_1:13;
hence contradiction by A1, A3, MCART_1:13; :: thesis: verum