let a, b be set ; :: thesis: ( a <> b iff {[a,b]} misses {[a,a],[b,b]} )
thus ( a <> b implies {[a,b]} misses {[a,a],[b,b]} ) :: thesis: ( {[a,b]} misses {[a,a],[b,b]} implies a <> b )

proof

assume A0: a <> b ; :: thesis: {[a,b]} misses {[a,a],[b,b]}
then A1: [a,b] <> [a,a] by XTUPLE_0:1;
A2: [a,b] <> [b,b] by A0, XTUPLE_0:1;
set A = {[a,b]};
set B = {[a,a],[b,b]};
assume {[a,b]} meets {[a,a],[b,b]} ; :: thesis: contradiction
then consider x being object such that
A4: ( x in {[a,b]} & x in {[a,a],[b,b]} ) by XBOOLE_0:3;
x = [a,b] by TARSKI:def 1, A4;
hence contradiction by A1, A2, A4, TARSKI:def 2; :: thesis: verum

end;

assume A0: {[a,b]} misses {[a,a],[b,b]} ; :: thesis: a <> b
assume a = b ; :: thesis: contradiction
then not [a,a] in {[a,a],[b,b]} by ZFMISC_1:48, A0;
hence contradiction by TARSKI:def 2; :: thesis: verum