defpred S1[ object , object ] means ex p, q, s, t being object st
( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R );
let A, B be Relation; ( ( for x, y being object holds
( [x,y] in A iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being object holds
( [x,y] in B iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) implies A = B )
assume that
A7:
for x, y being object holds
( [x,y] in A iff S1[x,y] )
and
A8:
for x, y being object holds
( [x,y] in B iff S1[x,y] )
; A = B
thus
A = B
from RELAT_1:sch 2(A7, A8); verum