set U = union_of R,S;
set cU = the carrier of (union_of R,S);
set IU = the InternalRel of (union_of R,S);
set cR = the carrier of R;
set cS = the carrier of S;
let x, y be set ; :: according to NECKLACE:def 4,RELAT_2:def 3 :: thesis: ( not x in the carrier of (union_of R,S) or not y in the carrier of (union_of R,S) or not [x,y] in the InternalRel of (union_of R,S) or [y,x] in the InternalRel of (union_of R,S) )
assume ( x in the carrier of (union_of R,S) & y in the carrier of (union_of R,S) & [x,y] in the InternalRel of (union_of R,S) ) ; :: thesis: [y,x] in the InternalRel of (union_of R,S)
then A1: [x,y] in the InternalRel of R \/ the InternalRel of S by NECKLA_2:def 2;

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

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

A3: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 4;
( x in the carrier of R & y in the carrier of R ) by A2, ZFMISC_1:106;
then [y,x] in the InternalRel of R by A2, A3, RELAT_2:def 3;
then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;
hence [y,x] in the InternalRel of (union_of R,S) by NECKLA_2:def 2; :: thesis: verum

end;

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

A5: the InternalRel of S is_symmetric_in the carrier of S by NECKLACE:def 4;
( x in the carrier of S & y in the carrier of S ) by A4, ZFMISC_1:106;
then [y,x] in the InternalRel of S by A4, A5, RELAT_2:def 3;
then [y,x] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;
hence [y,x] in the InternalRel of (union_of R,S) by NECKLA_2:def 2; :: thesis: verum

end;

end;