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) )
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;
assume that
x in the carrier of (union_of R,S) and
y in the carrier of (union_of R,S) and
A1: [x,y] in the InternalRel of (union_of R,S) ; :: thesis: [y,x] in the InternalRel of (union_of R,S)
A2: [x,y] in the InternalRel of R \/ the InternalRel of S by A1, NECKLA_2:def 2;

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

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

A4: 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 A3, ZFMISC_1:106;
then [y,x] in the InternalRel of R by A3, A4, 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 A5: [x,y] in the InternalRel of S ; :: thesis: [y,x] in the InternalRel of (union_of R,S)

A6: 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 A5, ZFMISC_1:106;
then [y,x] in the InternalRel of S by A5, A6, 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;