let x, y be object ; :: thesis: {[x,y]} ~ = {[y,x]}
set Z = {[x,y]} ~ ;

now :: thesis: for a, b being object holds
( ( [a,b] in {[x,y]} ~ implies [a,b] in {[y,x]} ) & ( [a,b] in {[y,x]} implies [a,b] in {[x,y]} ~ ) )

let a, b be object ; :: thesis: ( ( [a,b] in {[x,y]} ~ implies [a,b] in {[y,x]} ) & ( [a,b] in {[y,x]} implies [a,b] in {[x,y]} ~ ) )

hereby :: thesis: ( [a,b] in {[y,x]} implies [a,b] in {[x,y]} ~ )

assume [a,b] in {[x,y]} ~ ; :: thesis: [a,b] in {[y,x]}
then [b,a] in {[x,y]} by RELAT_1:def 7;
then [b,a] = [x,y] by TARSKI:def 1;
then ( b = x & a = y ) by XTUPLE_0:1;
hence [a,b] in {[y,x]} by TARSKI:def 1; :: thesis: verum

end;

assume [a,b] in {[y,x]} ; :: thesis: [a,b] in {[x,y]} ~
then [a,b] = [y,x] by TARSKI:def 1;
then ( a = y & b = x ) by XTUPLE_0:1;
then [b,a] in {[x,y]} by TARSKI:def 1;
hence [a,b] in {[x,y]} ~ by RELAT_1:def 7; :: thesis: verum

end;

hence {[x,y]} ~ = {[y,x]} by RELAT_1:def 2; :: thesis: verum