defpred S₁[ 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; :: thesis: ( ( 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 S₁[x,y] ) and
A8: for x, y being object holds
( [x,y] in B iff S₁[x,y] ) ; :: thesis: A = B
thus A = B from RELAT_1:sch 2(A7, A8); :: thesis: verum