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