set SU = sum_of (R,S);
set cSU = the carrier of (sum_of (R,S));
set ISU = the InternalRel of (sum_of (R,S));
set cR = the carrier of R;
set IR = the InternalRel of R;
set cS = the carrier of S;
set IS = the InternalRel of S;
A7:
the InternalRel of S is_symmetric_in the carrier of S
by NECKLACE:def 3;
A8:
the InternalRel of R is_symmetric_in the carrier of R
by NECKLACE:def 3;
the InternalRel of (sum_of (R,S)) is_symmetric_in the carrier of (sum_of (R,S))
proof
let x,
y be
object ;
RELAT_2:def 3 ( not x in the carrier of (sum_of (R,S)) or not y in the carrier of (sum_of (R,S)) or not [x,y] in the InternalRel of (sum_of (R,S)) or [y,x] in the InternalRel of (sum_of (R,S)) )
assume that
x in the
carrier of
(sum_of (R,S))
and
y in the
carrier of
(sum_of (R,S))
and A9:
[x,y] in the
InternalRel of
(sum_of (R,S))
;
[y,x] in the InternalRel of (sum_of (R,S))
[x,y] 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 A9, NECKLA_2:def 3;
then
(
[x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:] or
[x,y] in [: the carrier of S, the carrier of R:] )
by XBOOLE_0:def 3;
then A10:
(
[x,y] in the
InternalRel of
R \/ the
InternalRel of
S or
[x,y] in [: the carrier of R, the carrier of S:] or
[x,y] in [: the carrier of S, the carrier of R:] )
by XBOOLE_0:def 3;
per cases
( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or [x,y] in [: the carrier of R, the carrier of S:] or [x,y] in [: the carrier of S, the carrier of R:] )
by A10, XBOOLE_0:def 3;
suppose A11:
[x,y] in the
InternalRel of
R
;
[y,x] in the InternalRel of (sum_of (R,S))then
(
x in the
carrier of
R &
y in the
carrier of
R )
by ZFMISC_1:87;
then
[y,x] in the
InternalRel of
R
by A8, A11;
then
[y,x] in the
InternalRel of
R \/ the
InternalRel of
S
by XBOOLE_0:def 3;
then
[y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]
by XBOOLE_0:def 3;
then
[y,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 XBOOLE_0:def 3;
hence
[y,x] in the
InternalRel of
(sum_of (R,S))
by NECKLA_2:def 3;
verum end; suppose A12:
[x,y] in the
InternalRel of
S
;
[y,x] in the InternalRel of (sum_of (R,S))then
(
x in the
carrier of
S &
y in the
carrier of
S )
by ZFMISC_1:87;
then
[y,x] in the
InternalRel of
S
by A7, A12;
then
[y,x] in the
InternalRel of
R \/ the
InternalRel of
S
by XBOOLE_0:def 3;
then
[y,x] in ( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]
by XBOOLE_0:def 3;
then
[y,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 XBOOLE_0:def 3;
hence
[y,x] in the
InternalRel of
(sum_of (R,S))
by NECKLA_2:def 3;
verum end; suppose
[x,y] in [: the carrier of R, the carrier of S:]
;
[y,x] in the InternalRel of (sum_of (R,S))then
(
x in the
carrier of
R &
y in the
carrier of
S )
by ZFMISC_1:87;
then
[y,x] in [: the carrier of S, the carrier of R:]
by ZFMISC_1:87;
then
[y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]
by XBOOLE_0:def 3;
then
[y,x] in the
InternalRel of
S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])
by XBOOLE_0:def 3;
then
[y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]
by XBOOLE_1:4;
then
[y,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 XBOOLE_0:def 3;
then
[y,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 XBOOLE_1:4;
then
[y,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 XBOOLE_1:4;
then
[y,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 XBOOLE_1:4;
hence
[y,x] in the
InternalRel of
(sum_of (R,S))
by NECKLA_2:def 3;
verum end; suppose
[x,y] in [: the carrier of S, the carrier of R:]
;
[y,x] in the InternalRel of (sum_of (R,S))then
(
x in the
carrier of
S &
y in the
carrier of
R )
by ZFMISC_1:87;
then
[y,x] in [: the carrier of R, the carrier of S:]
by ZFMISC_1:87;
then
[y,x] in [: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:]
by XBOOLE_0:def 3;
then
[y,x] in the
InternalRel of
S \/ ([: the carrier of R, the carrier of S:] \/ [: the carrier of S, the carrier of R:])
by XBOOLE_0:def 3;
then
[y,x] in ( the InternalRel of S \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:]
by XBOOLE_1:4;
then
[y,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 XBOOLE_0:def 3;
then
[y,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 XBOOLE_1:4;
then
[y,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 XBOOLE_1:4;
then
[y,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 XBOOLE_1:4;
hence
[y,x] in the
InternalRel of
(sum_of (R,S))
by NECKLA_2:def 3;
verum end;
end;
hence
sum_of (R,S) is symmetric
; verum