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