let G1, G2 be RelStr ; :: thesis:
assume A1: the carrier of G1 misses the carrier of G2 ; :: thesis:
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:121 ;
A3: for a, b being set 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 set ; :: thesis:
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)) ) :: thesis:

proof

assume [a,b] in the InternalRel of (ComplRelStr (sum_of G1,G2)) ; :: thesis:
then A4: [a,b] in (the InternalRel of (sum_of G1,G2) ` ) \ (id the carrier of (sum_of G1,G2)) by NECKLACE:def 9;
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 5;
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:] ) ; :: thesis:
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; :: thesis:

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

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 5;
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 9;
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; :: thesis:

end;

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

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

end;

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

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

end;

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

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 5;
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 9;
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; :: thesis:

end;

assume [a,b] in the InternalRel of (union_of (ComplRelStr G1),(ComplRelStr G2)) ; :: thesis:
then A11: [a,b] in the InternalRel of (ComplRelStr G1) \/ the InternalRel of (ComplRelStr G2) by NECKLA_2:def 2;

per cases 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) ; :: thesis:

then A12: [a,b] in (the InternalRel of G1 ` ) \ (id the carrier of G1) by NECKLACE:def 9;
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)

proof

assume [a,b] in id the carrier of (sum_of G1,G2) ; :: thesis:
then [a,b] in id (the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 3;
then [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:32;
then [a,b] in id the carrier of G2 by A13, XBOOLE_0:def 3;
then A15: a in the carrier of G2 by ZFMISC_1:106;
a in the carrier of G1 by A12, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A15, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

[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 5;
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) ; :: thesis:
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;

per cases 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:] ) by A16, A18, XBOOLE_0:def 3;

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

A20: a in the carrier of G1 by A12, ZFMISC_1:106;
a in the carrier of G2 by A19, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A20, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

suppose A21: [a,b] in [:the carrier of G1,the carrier of G2:] ; :: thesis:

A22: b in the carrier of G1 by A12, ZFMISC_1:106;
b in the carrier of G2 by A21, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A22, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

suppose A23: [a,b] in [:the carrier of G2,the carrier of G1:] ; :: thesis:

A24: a in the carrier of G1 by A12, ZFMISC_1:106;
a in the carrier of G2 by A23, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A24, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

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 5;
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 9; :: thesis:

end;

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

then A25: [a,b] in (the InternalRel of G2 ` ) \ (id the carrier of G2) by NECKLACE:def 9;
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)

proof

assume [a,b] in id the carrier of (sum_of G1,G2) ; :: thesis:
then [a,b] in id (the carrier of G1 \/ the carrier of G2) by NECKLA_2:def 3;
then [a,b] in (id the carrier of G1) \/ (id the carrier of G2) by SYSREL:32;
then [a,b] in id the carrier of G1 by A26, XBOOLE_0:def 3;
then A28: b in the carrier of G1 by ZFMISC_1:106;
b in the carrier of G2 by A25, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A28, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

[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 5;
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) ; :: thesis:
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;

per cases in the InternalRel 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:] ) by A29, A31, XBOOLE_0:def 3;

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

A33: a in the carrier of G2 by A25, ZFMISC_1:106;
a in the carrier of G1 by A32, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A33, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

suppose A34: [a,b] in [:the carrier of G1,the carrier of G2:] ; :: thesis:

A35: a in the carrier of G2 by A25, ZFMISC_1:106;
a in the carrier of G1 by A34, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A35, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

suppose A36: [a,b] in [:the carrier of G2,the carrier of G1:] ; :: thesis:

A37: b in the carrier of G2 by A25, ZFMISC_1:106;
b in the carrier of G1 by A36, ZFMISC_1:106;
then not the carrier of G1 /\ the carrier of G2 is empty by A37, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

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 5;
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 9; :: thesis:

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 9
.= the carrier of G1 \/ the carrier of G2 by NECKLACE:def 9 ;
the carrier of (ComplRelStr (sum_of G1,G2)) = the carrier of (sum_of G1,G2) by NECKLACE:def 9
.= 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; :: thesis: