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)

proof

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

per cases ( [x,x] 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: contradiction

then x in the carrier of R by ZFMISC_1:106;
hence contradiction by A2, NECKLACE:def 6; :: thesis: verum

end;

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

then x in the carrier of S by ZFMISC_1:106;
hence contradiction by A3, NECKLACE:def 6; :: thesis: verum

end;

end;

end;

hence union_of R,S is irreflexive by NECKLACE:def 6; :: thesis: verum