let a, b be set ; :: thesis: ( a <> b implies {[a,a],[b,b]} <> {[a,a],[a,b],[b,a],[b,b]} )
assume AA: a <> b ; :: thesis: {[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; :: thesis: verum