let x be object ; RELAT_2:def 1,RELAT_2:def 9 ( not x in field [^R,S^] or [^,^] in [^R,S^] )
assume
x in field [^R,S^]
; [^,^] 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;
R1 = field R
by ORDERS_1:12;
then
R is_reflexive_in R1
by RELAT_2:def 9;
then
[x1,x1] in R
by A1;
hence
[^,^] in [^R,S^]
by A1, A2, A3, Def3; verum