set SU = sum_of (R,S);

set cSU = the carrier of (sum_of (R,S));

set ISU = the InternalRel of (sum_of (R,S));

set cR = the carrier of R;

set IR = the InternalRel of R;

set cS = the carrier of S;

set IS = the InternalRel of S;

A7: the InternalRel of S is_symmetric_in the carrier of S by NECKLACE:def 3;

A8: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;

the InternalRel of (sum_of (R,S)) is_symmetric_in the carrier of (sum_of (R,S))

set cSU = the carrier of (sum_of (R,S));

set ISU = the InternalRel of (sum_of (R,S));

set cR = the carrier of R;

set IR = the InternalRel of R;

set cS = the carrier of S;

set IS = the InternalRel of S;

A7: the InternalRel of S is_symmetric_in the carrier of S by NECKLACE:def 3;

A8: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;

the InternalRel of (sum_of (R,S)) is_symmetric_in the carrier of (sum_of (R,S))

proof

hence
sum_of (R,S) is symmetric
; :: thesis: verum
let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of (sum_of (R,S)) or not y in the carrier of (sum_of (R,S)) or not [x,y] in the InternalRel of (sum_of (R,S)) or [y,x] in the InternalRel of (sum_of (R,S)) )

assume that

x in the carrier of (sum_of (R,S)) and

y in the carrier of (sum_of (R,S)) and

A9: [x,y] in the InternalRel of (sum_of (R,S)) ; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

[x,y] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by A9, NECKLA_2:def 3;

then ( [x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;

then A10: ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;

end;assume that

x in the carrier of (sum_of (R,S)) and

y in the carrier of (sum_of (R,S)) and

A9: [x,y] in the InternalRel of (sum_of (R,S)) ; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

[x,y] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by A9, NECKLA_2:def 3;

then ( [x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;

then A10: ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;

per cases
( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or [x,y] in [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] )
by A10, XBOOLE_0:def 3;

end;

suppose A11:
[x,y] in the InternalRel of R
; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

then
( x in the carrier of R & y in the carrier of R )
by ZFMISC_1:87;

then [y,x] in the InternalRel of R by A8, A11;

then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] by XBOOLE_0:def 3;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

end;then [y,x] in the InternalRel of R by A8, A11;

then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] by XBOOLE_0:def 3;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

suppose A12:
[x,y] in the InternalRel of S
; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

then
( x in the carrier of S & y in the carrier of S )
by ZFMISC_1:87;

then [y,x] in the InternalRel of S by A7, A12;

then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] by XBOOLE_0:def 3;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

end;then [y,x] in the InternalRel of S by A7, A12;

then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] by XBOOLE_0:def 3;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

suppose
[x,y] in [: the carrier of R, the carrier of S:]
; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

then
( x in the carrier of R & y in the carrier of S )
by ZFMISC_1:87;

then [y,x] in [: the carrier of S, the carrier of R:] by ZFMISC_1:87;

then [y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

then [y,x] in the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

then [y,x] in the InternalRel of R \/ (( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in the InternalRel of R \/ ( the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])) by XBOOLE_1:4;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_1:4;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

end;then [y,x] in [: the carrier of S, the carrier of R:] by ZFMISC_1:87;

then [y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

then [y,x] in the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

then [y,x] in the InternalRel of R \/ (( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in the InternalRel of R \/ ( the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])) by XBOOLE_1:4;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_1:4;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

suppose
[x,y] in [: the carrier of S, the carrier of R:]
; :: thesis: [y,x] in the InternalRel of (sum_of (R,S))

then
( x in the carrier of S & y in the carrier of R )
by ZFMISC_1:87;

then [y,x] in [: the carrier of R, the carrier of S:] by ZFMISC_1:87;

then [y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

then [y,x] in the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

then [y,x] in the InternalRel of R \/ (( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in the InternalRel of R \/ ( the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])) by XBOOLE_1:4;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_1:4;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum

end;then [y,x] in [: the carrier of R, the carrier of S:] by ZFMISC_1:87;

then [y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:] by XBOOLE_0:def 3;

then [y,x] in the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

then [y,x] in the InternalRel of R \/ (( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]) by XBOOLE_0:def 3;

then [y,x] in the InternalRel of R \/ ( the InternalRel of S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])) by XBOOLE_1:4;

then [y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]) by XBOOLE_1:4;

then [y,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by XBOOLE_1:4;

hence [y,x] in the InternalRel of (sum_of (R,S)) by NECKLA_2:def 3; :: thesis: verum