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))

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

hence
union_of (R,S) is irreflexive
; :: thesis: verum
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;

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

end;

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

then
x in the carrier of R
by ZFMISC_1:87;

hence contradiction by A2, NECKLACE:def 5; :: thesis: verum

end;hence contradiction by A2, NECKLACE:def 5; :: thesis: verum

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

then
x in the carrier of S
by ZFMISC_1:87;

hence contradiction by A3, NECKLACE:def 5; :: thesis: verum

end;hence contradiction by A3, NECKLACE:def 5; :: thesis: verum