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 x in field [^R,S^] ; :: thesis: [^,^] in [^R,S^]
then consider x1, x2 being object such that
A1: x1 in R1 and
A2: x2 in S1 and
A3: x = [x1,x2] by ZFMISC_1:def 2;
S1 = field S by ORDERS_1:12;
then S is_reflexive_in S1 by RELAT_2:def 9;
then [x2,x2] in S by A2;
hence [^,^] in [^R,S^] by A1, A2, A3, Def3; :: thesis: verum