let x, y be object ; for X, Y being set st x <> y holds
[:X,{x}:] misses [:Y,{y}:]
let X, Y be set ; ( x <> y implies [:X,{x}:] misses [:Y,{y}:] )
assume A1:
x <> y
; [:X,{x}:] misses [:Y,{y}:]
assume
not [:X,{x}:] misses [:Y,{y}:]
; contradiction
then consider z being object 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; verum