consider Q being Relation of [:R1,S1:],[:R2,S2:] such that
A1: for x, y being object holds
( [x,y] in Q iff ( x in [:R1,S1:] & y in [:R2,S2:] & S₁[x,y] ) ) from RELSET_1:sch 1();
take Q ; :: thesis: for x, y being object holds
( [x,y] in Q 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 ) ) )
let x, y be object ; :: thesis: ( [x,y] in Q 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 ) ) )
thus ( [x,y] in Q implies S₁[x,y] ) by A1; :: thesis: ( 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 [x,y] in Q )
given r1, s1, r2, s2 being set such that A2: x = [r1,s1] and
A3: y = [r2,s2] and
A4: r1 in R1 and
A5: s1 in S1 and
A6: r2 in R2 and
A7: s2 in S2 and
A8: ( [r1,r2] in R or [s1,s2] in S ) ; :: thesis: [x,y] in Q
A9: x in [:R1,S1:] by A2, A4, A5, ZFMISC_1:87;
y in [:R2,S2:] by A3, A6, A7, ZFMISC_1:87;
hence [x,y] in Q by A1, A2, A3, A4, A5, A6, A7, A8, A9; :: thesis: verum