let G1, G2 be RelStr ; ( the carrier of G1 misses the carrier of G2 implies ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2)) )
assume A1:
the carrier of G1 misses the carrier of G2
; ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2))
set P = the InternalRel of (ComplRelStr (sum_of (G1,G2)));
set R = the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2)));
set X1 = the InternalRel of (ComplRelStr G1);
set X2 = the InternalRel of (ComplRelStr G2);
set X5 = [: the carrier of G1, the carrier of G1:];
set X6 = [: the carrier of G2, the carrier of G2:];
set X7 = [: the carrier of G1, the carrier of G2:];
set X8 = [: the carrier of G2, the carrier of G1:];
A2: [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):] =
[:( the carrier of G1 \/ the carrier of G2), the carrier of (sum_of (G1,G2)):]
by NECKLA_2:def 3
.=
[:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):]
by NECKLA_2:def 3
.=
(([: the carrier of G1, the carrier of G1:] \/ [: the carrier of G1, the carrier of G2:]) \/ [: the carrier of G2, the carrier of G1:]) \/ [: the carrier of G2, the carrier of G2:]
by ZFMISC_1:98
;
A3:
for a, b being object holds
( [a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2))) iff [a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2))) )
proof
let a,
b be
object ;
( [a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2))) iff [a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2))) )
set x =
[a,b];
thus
(
[a,b] in the
InternalRel of
(ComplRelStr (sum_of (G1,G2))) implies
[a,b] in the
InternalRel of
(union_of ((ComplRelStr G1),(ComplRelStr G2))) )
( [a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2))) implies [a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2))) )proof
assume
[a,b] in the
InternalRel of
(ComplRelStr (sum_of (G1,G2)))
;
[a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2)))
then A4:
[a,b] in ( the InternalRel of (sum_of (G1,G2)) `) \ (id the carrier of (sum_of (G1,G2)))
by NECKLACE:def 8;
then
(
[a,b] in ([: the carrier of G1, the carrier of G1:] \/ [: the carrier of G1, the carrier of G2:]) \/ [: the carrier of G2, the carrier of G1:] or
[a,b] in [: the carrier of G2, the carrier of G2:] )
by A2, XBOOLE_0:def 3;
then A5:
(
[a,b] in [: the carrier of G1, the carrier of G1:] \/ [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] or
[a,b] in [: the carrier of G2, the carrier of G2:] )
by XBOOLE_0:def 3;
[a,b] in the
InternalRel of
(sum_of (G1,G2)) `
by A4, XBOOLE_0:def 5;
then
[a,b] in [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):] \ the
InternalRel of
(sum_of (G1,G2))
by SUBSET_1:def 4;
then
not
[a,b] in the
InternalRel of
(sum_of (G1,G2))
by XBOOLE_0:def 5;
then A6:
not
[a,b] in (( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:]) \/ [: the carrier of G2, the carrier of G1:]
by NECKLA_2:def 3;
A7:
( not
[a,b] in the
InternalRel of
G1 & not
[a,b] in the
InternalRel of
G2 & not
[a,b] in [: the carrier of G1, the carrier of G2:] & not
[a,b] in [: the carrier of G2, the carrier of G1:] )
proof
assume
(
[a,b] in the
InternalRel of
G1 or
[a,b] in the
InternalRel of
G2 or
[a,b] in [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
;
contradiction
then
(
[a,b] in the
InternalRel of
G1 \/ the
InternalRel of
G2 or
[a,b] in [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
then
(
[a,b] in ( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
hence
contradiction
by A6, XBOOLE_0:def 3;
verum
end;
not
[a,b] in id the
carrier of
(sum_of (G1,G2))
by A4, XBOOLE_0:def 5;
then
not
[a,b] in id ( the carrier of G1 \/ the carrier of G2)
by NECKLA_2:def 3;
then A8:
not
[a,b] in (id the carrier of G1) \/ (id the carrier of G2)
by SYSREL:14;
then A9:
not
[a,b] in id the
carrier of
G1
by XBOOLE_0:def 3;
A10:
not
[a,b] in id the
carrier of
G2
by A8, XBOOLE_0:def 3;
per cases
( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of G1, the carrier of G2:] or [a,b] in [: the carrier of G2, the carrier of G1:] or [a,b] in [: the carrier of G2, the carrier of G2:] )
by A5, XBOOLE_0:def 3;
suppose
[a,b] in [: the carrier of G1, the carrier of G1:]
;
[a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2)))then
[a,b] in [: the carrier of G1, the carrier of G1:] \ the
InternalRel of
G1
by A7, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
G1 `
by SUBSET_1:def 4;
then
[a,b] in ( the InternalRel of G1 `) \ (id the carrier of G1)
by A9, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
(ComplRelStr G1)
by NECKLACE:def 8;
then
[a,b] in the
InternalRel of
(ComplRelStr G1) \/ the
InternalRel of
(ComplRelStr G2)
by XBOOLE_0:def 3;
hence
[a,b] in the
InternalRel of
(union_of ((ComplRelStr G1),(ComplRelStr G2)))
by NECKLA_2:def 2;
verum end; suppose
[a,b] in [: the carrier of G2, the carrier of G2:]
;
[a,b] in the InternalRel of (union_of ((ComplRelStr G1),(ComplRelStr G2)))then
[a,b] in [: the carrier of G2, the carrier of G2:] \ the
InternalRel of
G2
by A7, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
G2 `
by SUBSET_1:def 4;
then
[a,b] in ( the InternalRel of G2 `) \ (id the carrier of G2)
by A10, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
(ComplRelStr G2)
by NECKLACE:def 8;
then
[a,b] in the
InternalRel of
(ComplRelStr G1) \/ the
InternalRel of
(ComplRelStr G2)
by XBOOLE_0:def 3;
hence
[a,b] in the
InternalRel of
(union_of ((ComplRelStr G1),(ComplRelStr G2)))
by NECKLA_2:def 2;
verum end; end;
end;
assume
[a,b] in the
InternalRel of
(union_of ((ComplRelStr G1),(ComplRelStr G2)))
;
[a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2)))
then A11:
[a,b] in the
InternalRel of
(ComplRelStr G1) \/ the
InternalRel of
(ComplRelStr G2)
by NECKLA_2:def 2;
per cases
( [a,b] in the InternalRel of (ComplRelStr G1) or [a,b] in the InternalRel of (ComplRelStr G2) )
by A11, XBOOLE_0:def 3;
suppose
[a,b] in the
InternalRel of
(ComplRelStr G1)
;
[a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2)))then A12:
[a,b] in ( the InternalRel of G1 `) \ (id the carrier of G1)
by NECKLACE:def 8;
then A13:
not
[a,b] in id the
carrier of
G1
by XBOOLE_0:def 5;
A14:
not
[a,b] in id the
carrier of
(sum_of (G1,G2))
[a,b] in the
InternalRel of
G1 `
by A12, XBOOLE_0:def 5;
then
[a,b] in [: the carrier of G1, the carrier of G1:] \ the
InternalRel of
G1
by SUBSET_1:def 4;
then A16:
not
[a,b] in the
InternalRel of
G1
by XBOOLE_0:def 5;
A17:
not
[a,b] in the
InternalRel of
(sum_of (G1,G2))
proof
assume
[a,b] in the
InternalRel of
(sum_of (G1,G2))
;
contradiction
then
[a,b] in (( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:]) \/ [: the carrier of G2, the carrier of G1:]
by NECKLA_2:def 3;
then
(
[a,b] in ( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
then A18:
(
[a,b] in the
InternalRel of
G1 \/ the
InternalRel of
G2 or
[a,b] in [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
end;
[a,b] in [: the carrier of G1, the carrier of G1:] \/ (([: the carrier of G1, the carrier of G2:] \/ [: the carrier of G2, the carrier of G1:]) \/ [: the carrier of G2, the carrier of G2:])
by A12, XBOOLE_0:def 3;
then
[a,b] in [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):]
by A2, XBOOLE_1:113;
then
[a,b] in [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):] \ the
InternalRel of
(sum_of (G1,G2))
by A17, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
(sum_of (G1,G2)) `
by SUBSET_1:def 4;
then
[a,b] in ( the InternalRel of (sum_of (G1,G2)) `) \ (id the carrier of (sum_of (G1,G2)))
by A14, XBOOLE_0:def 5;
hence
[a,b] in the
InternalRel of
(ComplRelStr (sum_of (G1,G2)))
by NECKLACE:def 8;
verum end; suppose
[a,b] in the
InternalRel of
(ComplRelStr G2)
;
[a,b] in the InternalRel of (ComplRelStr (sum_of (G1,G2)))then A25:
[a,b] in ( the InternalRel of G2 `) \ (id the carrier of G2)
by NECKLACE:def 8;
then A26:
not
[a,b] in id the
carrier of
G2
by XBOOLE_0:def 5;
A27:
not
[a,b] in id the
carrier of
(sum_of (G1,G2))
[a,b] in the
InternalRel of
G2 `
by A25, XBOOLE_0:def 5;
then
[a,b] in [: the carrier of G2, the carrier of G2:] \ the
InternalRel of
G2
by SUBSET_1:def 4;
then A29:
not
[a,b] in the
InternalRel of
G2
by XBOOLE_0:def 5;
A30:
not
[a,b] in the
InternalRel of
(sum_of (G1,G2))
proof
assume
[a,b] in the
InternalRel of
(sum_of (G1,G2))
;
contradiction
then
[a,b] in (( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:]) \/ [: the carrier of G2, the carrier of G1:]
by NECKLA_2:def 3;
then
(
[a,b] in ( the InternalRel of G1 \/ the InternalRel of G2) \/ [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
then A31:
(
[a,b] in the
InternalRel of
G1 \/ the
InternalRel of
G2 or
[a,b] in [: the carrier of G1, the carrier of G2:] or
[a,b] in [: the carrier of G2, the carrier of G1:] )
by XBOOLE_0:def 3;
end;
[a,b] in [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):]
by A2, A25, XBOOLE_0:def 3;
then
[a,b] in [: the carrier of (sum_of (G1,G2)), the carrier of (sum_of (G1,G2)):] \ the
InternalRel of
(sum_of (G1,G2))
by A30, XBOOLE_0:def 5;
then
[a,b] in the
InternalRel of
(sum_of (G1,G2)) `
by SUBSET_1:def 4;
then
[a,b] in ( the InternalRel of (sum_of (G1,G2)) `) \ (id the carrier of (sum_of (G1,G2)))
by A27, XBOOLE_0:def 5;
hence
[a,b] in the
InternalRel of
(ComplRelStr (sum_of (G1,G2)))
by NECKLACE:def 8;
verum end; end;
end;
A38: the carrier of (union_of ((ComplRelStr G1),(ComplRelStr G2))) =
the carrier of (ComplRelStr G1) \/ the carrier of (ComplRelStr G2)
by NECKLA_2:def 2
.=
the carrier of G1 \/ the carrier of (ComplRelStr G2)
by NECKLACE:def 8
.=
the carrier of G1 \/ the carrier of G2
by NECKLACE:def 8
;
the carrier of (ComplRelStr (sum_of (G1,G2))) =
the carrier of (sum_of (G1,G2))
by NECKLACE:def 8
.=
the carrier of G1 \/ the carrier of G2
by NECKLA_2:def 3
;
hence
ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2))
by A38, A3, RELAT_1:def 2; verum