let R, S be irreflexive RelStr ; :: thesis:
assume A1: the carrier of R misses the carrier of S ; :: thesis:
for x being set st x in the carrier of (sum_of (R,S)) holds
not [x,x] in the InternalRel of (sum_of (R,S))

proof

set IR = the InternalRel of R;
set IS = the InternalRel of S;
set RS = [: the carrier of R, the carrier of S:];
set SR = [: the carrier of S, the carrier of R:];
let x be set ; :: thesis:
assume x in the carrier of (sum_of (R,S)) ; :: thesis:
assume [x,x] in the InternalRel of (sum_of (R,S)) ; :: thesis:
then [x,x] in (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] by NECKLA_2:def 3;
then ( [x,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] or [x,x] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;
then A2: ( [x,x] in the InternalRel of R \/ the InternalRel of S or [x,x] in [: the carrier of R, the carrier of S:] or [x,x] in [: the carrier of S, the carrier of R:] ) by XBOOLE_0:def 3;

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

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

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

end;

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

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

end;

suppose [x,x] in [: the carrier of R, the carrier of S:] ; :: thesis:

then ( x in the carrier of R & x in the carrier of S ) by ZFMISC_1:87;
hence contradiction by A1, XBOOLE_0:3; :: thesis:

end;

suppose [x,x] in [: the carrier of S, the carrier of R:] ; :: thesis:

then ( x in the carrier of S & x in the carrier of R ) by ZFMISC_1:87;
hence contradiction by A1, XBOOLE_0:3; :: thesis:

end;

end;

end;

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