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 ;
suppose [x,x] in [: the carrier of R, the carrier of S:] ; :: thesis: contradiction
end;
suppose [x,x] in [: the carrier of S, the carrier of R:] ; :: thesis: contradiction
end;
end;
end;
hence sum_of (R,S) is irreflexive ; :: thesis: verum