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;
for x being set st x in the carrier of (union_of (R,S)) holds
not [x,x] in the InternalRel of (union_of (R,S))

let x be set ; :: thesis:
assume x in the carrier of (union_of (R,S)) ; :: thesis:
assume [x,x] in the InternalRel of (union_of (R,S)) ; :: thesis:
then A1: [x,x] in the InternalRel of R \/ the InternalRel of S by NECKLA_2:def 2;

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

suppose A2: [x,x] in the InternalRel of R ; :: thesis:

then x in the carrier of R by ZFMISC_1:87;
hence contradiction by A2, NECKLACE:def 5; :: thesis:

end;

suppose A3: [x,x] in the InternalRel of S ; :: thesis:

then x in the carrier of S by ZFMISC_1:87;
hence contradiction by A3, NECKLACE:def 5; :: thesis:

end;

end;

end;

hence union_of (R,S) is irreflexive ; :: thesis: