let R, S be irreflexive RelStr ; :: thesis: ( the carrier of R misses the carrier of S implies sum_of R,S is irreflexive )
assume A1: the carrier of R misses the carrier of S ; :: thesis: sum_of R,S is irreflexive
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: ( x in the carrier of (sum_of R,S) implies not [x,x] in the InternalRel of (sum_of R,S) )
assume x in the carrier of (sum_of R,S) ; :: thesis: not [x,x] in the InternalRel of (sum_of R,S)
assume [x,x] in the InternalRel of (sum_of R,S) ; :: thesis: contradiction
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 ( [x,x] 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: contradiction

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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