let X1, X2, Y1, Y2 be set ; :: thesis: ( ( for x, y being object holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) implies [:X1,Y1:] = [:X2,Y2:] )
assume A1: for x, y being object holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ; :: thesis: [:X1,Y1:] = [:X2,Y2:]

now :: thesis: for z being object holds
( ( z in [:X1,Y1:] implies z in [:X2,Y2:] ) & ( z in [:X2,Y2:] implies z in [:X1,Y1:] ) )

let z be object ; :: thesis: ( ( z in [:X1,Y1:] implies z in [:X2,Y2:] ) & ( z in [:X2,Y2:] implies z in [:X1,Y1:] ) )
thus ( z in [:X1,Y1:] implies z in [:X2,Y2:] ) :: thesis: ( z in [:X2,Y2:] implies z in [:X1,Y1:] )

proof

assume A2: z in [:X1,Y1:] ; :: thesis: z in [:X2,Y2:]
then ex x, y being object st
( x in X1 & y in Y1 & [x,y] = z ) by Def2;
hence z in [:X2,Y2:] by A1, A2; :: thesis: verum

end;

assume A3: z in [:X2,Y2:] ; :: thesis: z in [:X1,Y1:]
then ex x, y being object st
( x in X2 & y in Y2 & [x,y] = z ) by Def2;
hence z in [:X1,Y1:] by A1, A3; :: thesis: verum

end;

hence [:X1,Y1:] = [:X2,Y2:] by TARSKI:2; :: thesis: verum