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

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

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

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

end;

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

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

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

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

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

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

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

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

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:87;

hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

end;hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

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:87;

hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

end;hence contradiction by A1, XBOOLE_0:3; :: thesis: verum