thus ( P = R implies for a, b being set holds
( [a,b] in P iff [a,b] in R ) ) ; :: thesis: ( ( for a, b being set holds
( [a,b] in P iff [a,b] in R ) ) implies P = R )
thus ( ( for a, b being set holds
( [a,b] in P iff [a,b] in R ) ) implies P = R ) :: thesis: verum

proof

assume A1: for a, b being set holds
( [a,b] in P iff [a,b] in R ) ; :: thesis: P = R

now

let x be set ; :: thesis: ( x in P iff x in R )

A2: now

assume A3: x in R ; :: thesis: x in P
then ex y, z being set st x = [y,z] by Def1;
hence x in P by A1, A3; :: thesis: verum

end;

now

assume A4: x in P ; :: thesis: x in R
then ex y, z being set st x = [y,z] by Def1;
hence x in R by A1, A4; :: thesis: verum

end;

hence ( x in P iff x in R ) by A2; :: thesis: verum

end;

hence P = R by TARSKI:2; :: thesis: verum

end;