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;
A6: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 4;
A7: the InternalRel of S is_symmetric_in the carrier of S by NECKLACE:def 4;
the InternalRel of (sum_of R,S) is_symmetric_in the carrier of (sum_of R,S)

proof

let x, y be set ; :: 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 ( x in the carrier of (sum_of R,S) & y in the carrier of (sum_of R,S) & [x,y] in the InternalRel of (sum_of R,S) ) ; :: thesis: [y,x] in the InternalRel of (sum_of R,S)
then [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 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 A8: ( [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 A8, XBOOLE_0:def 3;

suppose A9: [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:106;
then [y,x] in the InternalRel of R by A6, A9, RELAT_2:def 3;
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 A10: [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:106;
then [y,x] in the InternalRel of S by A7, A10, RELAT_2:def 3;
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:106;
then [y,x] in [:the carrier of S,the carrier of R:] by ZFMISC_1:106;
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:106;
then [y,x] in [:the carrier of R,the carrier of S:] by ZFMISC_1:106;
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 by NECKLACE:def 4; :: thesis: verum