let a, b be set ; ( a <> b implies {[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]} )
assume AA:
a <> b
; {[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]}
set x1 = [a,a];
set x2 = [a,b];
set x3 = [b,a];
set x4 = [b,b];
A0:
( [a,b] <> [a,a] & [a,b] <> [b,b] )
by AA, XTUPLE_0:1;
[a,b] in {[a,a],[a,b],[b,a],[b,b]}
by ENUMSET1:def 2;
hence
{[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]}
by A0, TARSKI:def 2; verum