let X, Y be set ; :: thesis: ( [:X,X:] = [:Y,Y:] implies X = Y )
assume A1: [:X,X:] = [:Y,Y:] ; :: thesis: X = Y
for x being set holds
( x in X iff x in Y )

proof

let x be set ; :: thesis: ( x in X iff x in Y )
( ( x in X implies [x,x] in [:X,X:] ) & ( [x,x] in [:X,X:] implies x in X ) & ( x in Y implies [x,x] in [:Y,Y:] ) & ( [x,x] in [:Y,Y:] implies x in Y ) ) by Lm17;
hence ( x in X iff x in Y ) by A1; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum