let x be object ; RELAT_2:def 1,RELAT_2:def 9 ( not x in field [^R,S^] or [^,^] in [^R,S^] )
assume A1:
x in field [^R,S^]
; [^,^] 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^]
;
[^,^] 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;
end; suppose
x in rng [^R,S^]
;
[^,^] 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;
end;