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))

proof

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;

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;

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;

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;

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;

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;

end;

end;

hence sum_of (R,S) is symmetric ; :: thesis: verum