let A, B be Relation of [:R1,S1:],[:R2,S2:]; :: thesis: ( ( for x, y being object holds
( [x,y] in A iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) & ( for x, y being object holds
( [x,y] in B iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) implies A = B )
assume that
A10: for x, y being object holds
( [x,y] in A iff S₁[x,y] ) and
A11: 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(A10, A11); :: thesis: verum