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 9
.= the carrier of G1 \/ the carrier of G2 by NECKLACE:def 9 ;
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 set 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

let a, b be set ; :: 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)) )

proof

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

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

end;

( the carrier of G1 = the carrier of (ComplRelStr G1) & the carrier of G2 = the carrier of (ComplRelStr G2) ) by NECKLACE:def 9;
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:121;
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 5;
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;

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

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;

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;

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

end;

end;

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

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

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:] by XBOOLE_0:def 7;
hence contradiction by A2, ZFMISC_1:127; :: thesis: verum

end;

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

proof

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:32;
thus contradiction :: thesis: verum

proof

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;

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

hence contradiction by A13, XBOOLE_0:def 5; :: thesis: verum

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:] by XBOOLE_0:def 7;
hence contradiction by A2, ZFMISC_1:127; :: thesis: verum

end;

end;

end;

end;

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

end;

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

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:] by XBOOLE_0:def 7;
hence contradiction by A2, ZFMISC_1:127; :: thesis: verum

end;

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

proof

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

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;

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

hence contradiction by A18, XBOOLE_0:def 5; :: thesis: verum

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:] by XBOOLE_0:def 7;
hence contradiction by A2, ZFMISC_1:127; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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;

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

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

A28: b in the carrier of G2 by A24, ZFMISC_1:106;
b in the carrier of G1 by A27, ZFMISC_1:106;
then b in the carrier of G1 /\ the carrier of G2 by A28, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

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

A30: a in the carrier of G1 by A23, ZFMISC_1:106;
a in the carrier of G2 by A29, ZFMISC_1:106;
then a in the carrier of G1 /\ the carrier of G2 by A30, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

proof

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

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;

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

A34: b in the carrier of G2 by A24, ZFMISC_1:106;
b in the carrier of G1 by A33, ZFMISC_1:106;
then b in the carrier of G1 /\ the carrier of G2 by A34, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

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

A36: a in the carrier of G1 by A23, ZFMISC_1:106;
a in the carrier of G2 by A35, ZFMISC_1:106;
then a in the carrier of G1 /\ the carrier of G2 by A36, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

end;

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 9;
then A38: [a,b] in [:the carrier of G2,the carrier of G1:] by NECKLACE:def 9;
A39: not [a,b] in the InternalRel of (union_of G1,G2)

proof

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;

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

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

A42: a in the carrier of G2 by A37, ZFMISC_1:106;
a in the carrier of G1 by A41, ZFMISC_1:106;
then a in the carrier of G1 /\ the carrier of G2 by A42, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

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

A44: b in the carrier of G1 by A38, ZFMISC_1:106;
b in the carrier of G2 by A43, ZFMISC_1:106;
then b in the carrier of G1 /\ the carrier of G2 by A44, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

proof

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

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;

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

A48: a in the carrier of G2 by A37, ZFMISC_1:106;
a in the carrier of G1 by A47, ZFMISC_1:106;
then a in the carrier of G1 /\ the carrier of G2 by A48, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

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

A50: b in the carrier of G1 by A38, ZFMISC_1:106;
b in the carrier of G2 by A49, ZFMISC_1:106;
then b in the carrier of G1 /\ the carrier of G2 by A50, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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