thus ( P = R implies for a, b being object holds
( [a,b] in P iff [a,b] in R ) ) ; :: thesis: ( ( for a, b being object holds
( [a,b] in P iff [a,b] in R ) ) implies P = R )
assume A1: for a, b being object holds
( [a,b] in P iff [a,b] in R ) ; :: thesis: P = R
thus P c= R :: according to XBOOLE_0:def 10 :: thesis: R c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in R )
assume A2: x in P ; :: thesis: x in R
then ex y, z being object st x = [y,z] by Def1;
hence x in R by A1, A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in P )
assume A3: x in R ; :: thesis: x in P
then ex y, z being object st x = [y,z] by Def1;
hence x in P by A1, A3; :: thesis: verum