let x, y be object ; RELAT_2:def 3,RELAT_2:def 11 ( not x in field [^R,S^] or not y in field [^R,S^] or not [^,^] in [^R,S^] or [^,^] in [^R,S^] )
assume that
x in field [^R,S^]
and
y in field [^R,S^]
; ( not [^,^] in [^R,S^] or [^,^] in [^R,S^] )
assume
[x,y] in [^R,S^]
; [^,^] in [^R,S^]
then consider p, q, s, t being set such that
A1:
x = [p,q]
and
A2:
y = [s,t]
and
A3:
p in R1
and
A4:
q in S1
and
A5:
s in R1
and
A6:
t in S1
and
A7:
( [p,s] in R or [q,t] in S )
by Def2;
A8:
R is_symmetric_in field R
by RELAT_2:def 11;
A9:
S is_symmetric_in field S
by RELAT_2:def 11;
per cases
( [p,s] in R or [q,t] in S )
by A7;
suppose A10:
[p,s] in R
;
[^,^] in [^R,S^]then A11:
p in field R
by RELAT_1:15;
s in field R
by A10, RELAT_1:15;
then
[s,p] in R
by A8, A10, A11;
hence
[^,^] in [^R,S^]
by A1, A2, A3, A4, A5, A6, Def2;
verum end; suppose A12:
[q,t] in S
;
[^,^] in [^R,S^]then A13:
q in field S
by RELAT_1:15;
t in field S
by A12, RELAT_1:15;
then
[t,q] in S
by A9, A12, A13;
hence
[^,^] in [^R,S^]
by A1, A2, A3, A4, A5, A6, Def2;
verum end;