let x, y be set ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field [^R,S^] or not y in field [^R,S^] or not [^,^] in [^R,S^] or [^,^] in [^R,S^] )
assume ( x in field [^R,S^] & y in field [^R,S^] ) ; :: thesis: ( not [^,^] in [^R,S^] or [^,^] in [^R,S^] )
assume [x,y] in [^R,S^] ; :: thesis: [^,^] in [^R,S^]
then consider p, q, s, t being set such that
A1: ( x = [p,q] & y = [s,t] ) and
A2: ( p in R1 & q in S1 & s in R1 & t in S1 ) and
A3: ( [p,s] in R or [q,t] in S ) by Def2;
A4: ( R is_symmetric_in field R & S is_symmetric_in field S ) by RELAT_2:def 11;

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

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

then ( p in field R & s in field R ) by RELAT_1:30;
then [s,p] in R by A4, A5, RELAT_2:def 3;
hence [^,^] in [^R,S^] by A1, A2, Def2; :: thesis: verum

end;

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

then ( q in field S & t in field S ) by RELAT_1:30;
then [t,q] in S by A4, A6, RELAT_2:def 3;
hence [^,^] in [^R,S^] by A1, A2, Def2; :: thesis: verum

end;

end;