let x, y be object ; :: according to NECKLACE:def 3,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;

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;

end;

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 3;

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

then [y,x] in the InternalRel of R by A3, A4;

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;( x in the carrier of R & y in the carrier of R ) by A3, ZFMISC_1:87;

then [y,x] in the InternalRel of R by A3, A4;

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

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 3;

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

then [y,x] in the InternalRel of S by A5, A6;

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;( x in the carrier of S & y in the carrier of S ) by A5, ZFMISC_1:87;

then [y,x] in the InternalRel of S by A5, A6;

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