let X1, X2, Y1, Y2 be set ; ( ( 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:] )
; [:X1,Y1:] = [:X2,Y2:]
now 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 ;
( ( 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:] )
( z in [:X2,Y2:] implies z in [:X1,Y1:] )assume A3:
z in [:X2,Y2:]
;
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;
verum end;
hence
[:X1,Y1:] = [:X2,Y2:]
by TARSKI:2; verum