let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field [^R,S^] or [^,^] in [^R,S^] )
assume A1: x in field [^R,S^] ; :: thesis: [^,^] in [^R,S^]
A2: R is_reflexive_in field R by RELAT_2:def 9;
A3: S is_reflexive_in field S by RELAT_2:def 9;

per cases ( x in dom [^R,S^] or x in rng [^R,S^] ) by A1, XBOOLE_0:def 3;

suppose x in dom [^R,S^] ; :: thesis: [^,^] in [^R,S^]

then consider y being object such that
A4: [x,y] in [^R,S^] by XTUPLE_0:def 12;
consider p, q, s, t being set such that
A5: x = [p,q] and
y = [s,t] and
A6: p in R1 and
A7: q in S1 and
s in R1 and
t in S1 and
A8: ( [p,s] in R or [q,t] in S ) by A4, Def2;

per cases ( [p,s] in R or [q,t] in S ) by A8;

suppose [p,s] in R ; :: thesis: [^,^] in [^R,S^]

then p in field R by RELAT_1:15;
then [p,p] in R by A2;
hence [^,^] in [^R,S^] by A5, A6, A7, Def2; :: thesis: verum

end;

suppose [q,t] in S ; :: thesis: [^,^] in [^R,S^]

then q in field S by RELAT_1:15;
then [q,q] in S by A3;
hence [^,^] in [^R,S^] by A5, A6, A7, Def2; :: thesis: verum

end;

end;

end;

suppose x in rng [^R,S^] ; :: thesis: [^,^] in [^R,S^]

then consider y being object such that
A9: [y,x] in [^R,S^] by XTUPLE_0:def 13;
consider p, q, s, t being set such that
y = [p,q] and
A10: x = [s,t] and
p in R1 and
q in S1 and
A11: s in R1 and
A12: t in S1 and
A13: ( [p,s] in R or [q,t] in S ) by A9, Def2;

per cases ( [p,s] in R or [q,t] in S ) by A13;

suppose [p,s] in R ; :: thesis: [^,^] in [^R,S^]

then s in field R by RELAT_1:15;
then [s,s] in R by A2;
hence [^,^] in [^R,S^] by A10, A11, A12, Def2; :: thesis: verum

end;

suppose [q,t] in S ; :: thesis: [^,^] in [^R,S^]

then t in field S by RELAT_1:15;
then [t,t] in S by A3;
hence [^,^] in [^R,S^] by A10, A11, A12, Def2; :: thesis: verum

end;

end;

end;

end;