let G1, G2 be RelStr ; :: thesis: ( the carrier of G1 misses the carrier of G2 implies ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2)) )

A1: the carrier of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) = the carrier of (ComplRelStr G1) \/ the carrier of (ComplRelStr G2) by NECKLA_2:def 3

.= 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 ;

set P = the InternalRel of (ComplRelStr (union_of (G1,G2)));

set R = the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)));

set X1 = the InternalRel of (ComplRelStr G1);

set X2 = the InternalRel of (ComplRelStr G2);

set X3 = [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):];

set X4 = [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):];

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

assume A2: the carrier of G1 misses the carrier of G2 ; :: thesis: ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2))

A3: for a, b being object holds

( [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) iff [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) )

.= the carrier of G1 \/ the carrier of G2 by NECKLA_2:def 2 ;

hence ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2)) by A1, A3, RELAT_1:def 2; :: thesis: verum

A1: the carrier of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) = the carrier of (ComplRelStr G1) \/ the carrier of (ComplRelStr G2) by NECKLA_2:def 3

.= 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 ;

set P = the InternalRel of (ComplRelStr (union_of (G1,G2)));

set R = the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)));

set X1 = the InternalRel of (ComplRelStr G1);

set X2 = the InternalRel of (ComplRelStr G2);

set X3 = [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):];

set X4 = [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):];

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

assume A2: the carrier of G1 misses the carrier of G2 ; :: thesis: ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2))

A3: for a, b being object holds

( [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) iff [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) )

proof

the carrier of (ComplRelStr (union_of (G1,G2))) =
the carrier of (union_of (G1,G2))
by NECKLACE:def 8
let a, b be object ; :: thesis: ( [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) iff [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) )

set x = [a,b];

thus ( [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) implies [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) ) :: thesis: ( [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) implies [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) )

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by NECKLA_2:def 3;

then ( [a,b] in ( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] ) by XBOOLE_0:def 3;

then A12: ( [a,b] in the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2) or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] ) by XBOOLE_0:def 3;

end;set x = [a,b];

thus ( [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) implies [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) ) :: thesis: ( [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) implies [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) )

proof

assume
[a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))
; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))
assume
[a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))
; :: thesis: [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))

then A4: [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by NECKLACE:def 8;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] ;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then A5: [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by NECKLA_2:def 2;

not [a,b] in id the carrier of (union_of (G1,G2)) by A4, XBOOLE_0:def 5;

then A6: not [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

A7: ( not [a,b] in id the carrier of G1 & not [a,b] in id the carrier of G2 )

then [a,b] in (([: the carrier of G1, the carrier of G1:] \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:] by A5, ZFMISC_1:98;

then [a,b] in [: the carrier of G1, the carrier of G1:] \/ (([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:]) by XBOOLE_1:113;

then ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in ([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:] ) by XBOOLE_0:def 3;

then ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ ([: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] \/ [: the carrier of G2, the carrier of G2:]) ) by XBOOLE_1:4;

then A8: ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] \/ [: the carrier of G2, the carrier of G2:] ) by XBOOLE_0:def 3;

[a,b] in the InternalRel of (union_of (G1,G2)) ` by A4, XBOOLE_0:def 5;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by SUBSET_1:def 4;

then not [a,b] in the InternalRel of (union_of (G1,G2)) by XBOOLE_0:def 5;

then A9: not [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then A10: not [a,b] in the InternalRel of G1 by XBOOLE_0:def 3;

A11: not [a,b] in the InternalRel of G2 by A9, XBOOLE_0:def 3;

end;then A4: [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by NECKLACE:def 8;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] ;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then A5: [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by NECKLA_2:def 2;

not [a,b] in id the carrier of (union_of (G1,G2)) by A4, XBOOLE_0:def 5;

then A6: not [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

A7: ( not [a,b] in id the carrier of G1 & not [a,b] in id the carrier of G2 )

proof

( the carrier of G1 = the carrier of (ComplRelStr G1) & the carrier of G2 = the carrier of (ComplRelStr G2) )
by NECKLACE:def 8;
assume
( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 )
; :: thesis: contradiction

then [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by XBOOLE_0:def 3;

hence contradiction by A6, SYSREL:14; :: thesis: verum

end;then [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by XBOOLE_0:def 3;

hence contradiction by A6, SYSREL:14; :: thesis: verum

then [a,b] in (([: the carrier of G1, the carrier of G1:] \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:] by A5, ZFMISC_1:98;

then [a,b] in [: the carrier of G1, the carrier of G1:] \/ (([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:]) by XBOOLE_1:113;

then ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in ([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) \/ [: the carrier of G2, the carrier of G2:] ) by XBOOLE_0:def 3;

then ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ ([: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] \/ [: the carrier of G2, the carrier of G2:]) ) by XBOOLE_1:4;

then A8: ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] \/ [: the carrier of G2, the carrier of G2:] ) by XBOOLE_0:def 3;

[a,b] in the InternalRel of (union_of (G1,G2)) ` by A4, XBOOLE_0:def 5;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by SUBSET_1:def 4;

then not [a,b] in the InternalRel of (union_of (G1,G2)) by XBOOLE_0:def 5;

then A9: not [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then A10: not [a,b] in the InternalRel of G1 by XBOOLE_0:def 3;

A11: not [a,b] in the InternalRel of G2 by A9, XBOOLE_0:def 3;

per cases
( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] or [a,b] in [: the carrier of G2, the carrier of G2:] )
by A8, XBOOLE_0:def 3;

end;

suppose
[a,b] in [: the carrier of G1, the carrier of G1:]
; :: thesis: [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))

then
[a,b] in [: the carrier of G1, the carrier of G1:] \ the InternalRel of G1
by A10, 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 A7, 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) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

end;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 A7, 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) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

suppose
[a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]
; :: thesis: [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))

then
[a,b] in the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]
by XBOOLE_0:def 3;

then [a,b] in ( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_0:def 3;

then [a,b] in the InternalRel of (ComplRelStr G1) \/ (( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

end;then [a,b] in ( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_0:def 3;

then [a,b] in the InternalRel of (ComplRelStr G1) \/ (( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

suppose
[a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]
; :: thesis: [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))

then
[a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]
by XBOOLE_0:def 3;

then [a,b] in the InternalRel of (ComplRelStr G2) \/ ([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in ( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:4;

then [a,b] in the InternalRel of (ComplRelStr G1) \/ (( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

end;then [a,b] in the InternalRel of (ComplRelStr G2) \/ ([: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in ( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:4;

then [a,b] in the InternalRel of (ComplRelStr G1) \/ (( the InternalRel of (ComplRelStr G2) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]) by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_1:113;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

suppose
[a,b] in [: the carrier of G2, the carrier of G2:]
; :: thesis: [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2)))

then
[a,b] in [: the carrier of G2, the carrier of G2:] \ the InternalRel of G2
by A11, 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 A7, 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;

then [a,b] in ( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_0:def 3;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

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

then [a,b] in ( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] by XBOOLE_0:def 3;

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by XBOOLE_0:def 3;

hence [a,b] in the InternalRel of (sum_of ((ComplRelStr G1),(ComplRelStr G2))) by NECKLA_2:def 3; :: thesis: verum

then [a,b] in (( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]) \/ [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] by NECKLA_2:def 3;

then ( [a,b] in ( the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2)) \/ [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] ) by XBOOLE_0:def 3;

then A12: ( [a,b] in the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2) or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] ) by XBOOLE_0:def 3;

per cases
( [a,b] in the InternalRel of (ComplRelStr G1) or [a,b] in the InternalRel of (ComplRelStr G2) or [a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):] or [a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):] )
by A12, XBOOLE_0:def 3;

end;

suppose
[a,b] in the InternalRel of (ComplRelStr G1)
; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))

then A13:
[a,b] in ( the InternalRel of G1 `) \ (id the carrier of G1)
by NECKLACE:def 8;

then [a,b] in the InternalRel of G1 ` by 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 A14: not [a,b] in the InternalRel of G1 by XBOOLE_0:def 5;

A15: not [a,b] in the InternalRel of (union_of (G1,G2))

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:] by XBOOLE_0:def 3;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A15, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A16, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

end;then [a,b] in the InternalRel of G1 ` by 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 A14: not [a,b] in the InternalRel of G1 by XBOOLE_0:def 5;

A15: not [a,b] in the InternalRel of (union_of (G1,G2))

proof

A16:
not [a,b] in id the carrier of (union_of (G1,G2))
assume
[a,b] in the InternalRel of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then [a,b] in the InternalRel of G2 by A14, XBOOLE_0:def 3;

then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by A13, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

end;then [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then [a,b] in the InternalRel of G2 by A14, XBOOLE_0:def 3;

then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by A13, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

proof

[a,b] in [: the carrier of G1, the carrier of G1:] \/ [: the carrier of G1, the carrier of G2:]
by A13, XBOOLE_0:def 3;
assume
[a,b] in id the carrier of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A17: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

thus contradiction :: thesis: verum

end;then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A17: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

thus contradiction :: thesis: verum

proof
end;

per cases
( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 )
by A17, XBOOLE_0:def 3;

end;

suppose
[a,b] in id the carrier of G2
; :: thesis: contradiction

then
not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty
by A13, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

end;then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

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:] by XBOOLE_0:def 3;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A15, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A16, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

suppose
[a,b] in the InternalRel of (ComplRelStr G2)
; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))

then A18:
[a,b] in ( the InternalRel of G2 `) \ (id the carrier of G2)
by NECKLACE:def 8;

then [a,b] in the InternalRel of G2 ` by 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 A19: not [a,b] in the InternalRel of G2 by XBOOLE_0:def 5;

A20: not [a,b] in the InternalRel of (union_of (G1,G2))

then [a,b] in [: 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 XBOOLE_0:def 3;

then [a,b] in ([: 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 XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:]) by XBOOLE_0:def 3;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_1:113;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A20, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A21, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

end;then [a,b] in the InternalRel of G2 ` by 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 A19: not [a,b] in the InternalRel of G2 by XBOOLE_0:def 5;

A20: not [a,b] in the InternalRel of (union_of (G1,G2))

proof

A21:
not [a,b] in id the carrier of (union_of (G1,G2))
assume
[a,b] in the InternalRel of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then [a,b] in the InternalRel of G1 by A19, XBOOLE_0:def 3;

then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by A18, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

end;then [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

then [a,b] in the InternalRel of G1 by A19, XBOOLE_0:def 3;

then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by A18, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

proof

[a,b] in [: the carrier of G2, the carrier of G1:] \/ [: the carrier of G2, the carrier of G2:]
by A18, XBOOLE_0:def 3;
assume
[a,b] in id the carrier of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A22: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

end;then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A22: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

per cases
( [a,b] in id the carrier of G2 or [a,b] in id the carrier of G1 )
by A22, XBOOLE_0:def 3;

end;

suppose
[a,b] in id the carrier of G1
; :: thesis: contradiction

then
not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty
by A18, XBOOLE_0:def 4;

then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

end;then [: the carrier of G1, the carrier of G1:] meets [: the carrier of G2, the carrier of G2:] ;

hence contradiction by A2, ZFMISC_1:104; :: thesis: verum

then [a,b] in [: 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 XBOOLE_0:def 3;

then [a,b] in ([: 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 XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:]) by XBOOLE_0:def 3;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_1:113;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A20, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A21, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

suppose
[a,b] in [: the carrier of (ComplRelStr G1), the carrier of (ComplRelStr G2):]
; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))

then A23:
[a,b] in [: the carrier of G1, the carrier of (ComplRelStr G2):]
by NECKLACE:def 8;

then A24: [a,b] in [: the carrier of G1, the carrier of G2:] by NECKLACE:def 8;

A25: not [a,b] in the InternalRel of (union_of (G1,G2))

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:]) by XBOOLE_0:def 3;

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:] by XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A25, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A31, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

end;then A24: [a,b] in [: the carrier of G1, the carrier of G2:] by NECKLACE:def 8;

A25: not [a,b] in the InternalRel of (union_of (G1,G2))

proof

A31:
not [a,b] in id the carrier of (union_of (G1,G2))
assume
[a,b] in the InternalRel of (union_of (G1,G2))
; :: thesis: contradiction

then A26: [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

end;then A26: [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

per cases
( [a,b] in the InternalRel of G1 or [a,b] in the InternalRel of G2 )
by A26, XBOOLE_0:def 3;

end;

suppose A27:
[a,b] in the InternalRel of G1
; :: thesis: contradiction

A28:
b in the carrier of G2
by A24, ZFMISC_1:87;

b in the carrier of G1 by A27, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A28, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;b in the carrier of G1 by A27, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A28, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

suppose A29:
[a,b] in the InternalRel of G2
; :: thesis: contradiction

A30:
a in the carrier of G1
by A23, ZFMISC_1:87;

a in the carrier of G2 by A29, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A30, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;a in the carrier of G2 by A29, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A30, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

proof

[a,b] in [: the carrier of G1, the carrier of G2:] \/ [: the carrier of G2, the carrier of G1:]
by A24, XBOOLE_0:def 3;
assume
[a,b] in id the carrier of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A32: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

end;then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A32: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

per cases
( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 )
by A32, XBOOLE_0:def 3;

end;

suppose A33:
[a,b] in id the carrier of G1
; :: thesis: contradiction

A34:
b in the carrier of G2
by A24, ZFMISC_1:87;

b in the carrier of G1 by A33, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A34, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;b in the carrier of G1 by A33, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A34, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

suppose A35:
[a,b] in id the carrier of G2
; :: thesis: contradiction

A36:
a in the carrier of G1
by A23, ZFMISC_1:87;

a in the carrier of G2 by A35, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A36, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;a in the carrier of G2 by A35, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A36, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

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:]) by XBOOLE_0:def 3;

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:] by XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A25, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A31, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

suppose
[a,b] in [: the carrier of (ComplRelStr G2), the carrier of (ComplRelStr G1):]
; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))

then A37:
[a,b] in [: the carrier of G2, the carrier of (ComplRelStr G1):]
by NECKLACE:def 8;

then A38: [a,b] in [: the carrier of G2, the carrier of G1:] by NECKLACE:def 8;

A39: not [a,b] in the InternalRel of (union_of (G1,G2))

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:]) by XBOOLE_0:def 3;

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:] by XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A39, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A45, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

end;then A38: [a,b] in [: the carrier of G2, the carrier of G1:] by NECKLACE:def 8;

A39: not [a,b] in the InternalRel of (union_of (G1,G2))

proof

A45:
not [a,b] in id the carrier of (union_of (G1,G2))
assume
[a,b] in the InternalRel of (union_of (G1,G2))
; :: thesis: contradiction

then A40: [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

end;then A40: [a,b] in the InternalRel of G1 \/ the InternalRel of G2 by NECKLA_2:def 2;

per cases
( [a,b] in the InternalRel of G1 or [a,b] in the InternalRel of G2 )
by A40, XBOOLE_0:def 3;

end;

suppose A41:
[a,b] in the InternalRel of G1
; :: thesis: contradiction

A42:
a in the carrier of G2
by A37, ZFMISC_1:87;

a in the carrier of G1 by A41, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A42, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;a in the carrier of G1 by A41, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A42, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

suppose A43:
[a,b] in the InternalRel of G2
; :: thesis: contradiction

A44:
b in the carrier of G1
by A38, ZFMISC_1:87;

b in the carrier of G2 by A43, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A44, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;b in the carrier of G2 by A43, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A44, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

proof

[a,b] in [: the carrier of G1, the carrier of G2:] \/ [: the carrier of G2, the carrier of G1:]
by A38, XBOOLE_0:def 3;
assume
[a,b] in id the carrier of (union_of (G1,G2))
; :: thesis: contradiction

then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A46: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

end;then [a,b] in id ( the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 2;

then A46: [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:14;

per cases
( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 )
by A46, XBOOLE_0:def 3;

end;

suppose A47:
[a,b] in id the carrier of G1
; :: thesis: contradiction

A48:
a in the carrier of G2
by A37, ZFMISC_1:87;

a in the carrier of G1 by A47, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A48, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;a in the carrier of G1 by A47, ZFMISC_1:87;

then a in the carrier of G1 /\ the carrier of G2 by A48, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

suppose A49:
[a,b] in id the carrier of G2
; :: thesis: contradiction

A50:
b in the carrier of G1
by A38, ZFMISC_1:87;

b in the carrier of G2 by A49, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A50, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;b in the carrier of G2 by A49, ZFMISC_1:87;

then b in the carrier of G1 /\ the carrier of G2 by A50, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

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:]) by XBOOLE_0:def 3;

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:] by XBOOLE_1:4;

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:]) \/ [: the carrier of G2, the carrier of G2:] by XBOOLE_0:def 3;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2),( the carrier of G1 \/ the carrier of G2):] by ZFMISC_1:98;

then [a,b] in [:( the carrier of G1 \/ the carrier of G2), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] by NECKLA_2:def 2;

then [a,b] in [: the carrier of (union_of (G1,G2)), the carrier of (union_of (G1,G2)):] \ the InternalRel of (union_of (G1,G2)) by A39, XBOOLE_0:def 5;

then [a,b] in the InternalRel of (union_of (G1,G2)) ` by SUBSET_1:def 4;

then [a,b] in ( the InternalRel of (union_of (G1,G2)) `) \ (id the carrier of (union_of (G1,G2))) by A45, XBOOLE_0:def 5;

hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum

.= the carrier of G1 \/ the carrier of G2 by NECKLA_2:def 2 ;

hence ComplRelStr (union_of (G1,G2)) = sum_of ((ComplRelStr G1),(ComplRelStr G2)) by A1, A3, RELAT_1:def 2; :: thesis: verum