let G1, G2 be RelStr ; :: thesis: ( the carrier of G1 misses the carrier of G2 implies ComplRelStr (union_of (G1,G2)) = sum_of ((),()) )
A1: the carrier of (sum_of ((),())) = the carrier of () \/ the carrier of () by NECKLA_2:def 3
.= the carrier of G1 \/ the carrier of () 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 ((),()));
set X1 = the InternalRel of ();
set X2 = the InternalRel of ();
set X3 = [: the carrier of (), the carrier of ():];
set X4 = [: the carrier of (), the carrier of ():];
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 ((),())
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 ((),())) )
proof
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 ((),())) )
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 ((),())) ) :: thesis: ( [a,b] in the InternalRel of (sum_of ((),())) 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 ((),()))
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 ;
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:14; :: thesis: verum
end;
( the carrier of G1 = the carrier of () & the carrier of G2 = the carrier of () ) by NECKLACE:def 8;
then [a,b] in (([: the carrier of G1, the carrier of G1:] \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of G2, the carrier of G2:] by ;
then [a,b] in [: the carrier of G1, the carrier of G1:] \/ (([: the carrier of (), the carrier of ():] \/ [: the carrier of (), the carrier of ():]) \/ [: 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 (), the carrier of ():] \/ [: the carrier of (), the carrier of ():]) \/ [: 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 (), the carrier of ():] \/ ([: the carrier of (), the carrier of ():] \/ [: 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 (), the carrier of ():] or [a,b] in [: the carrier of (), the carrier of ():] \/ [: the carrier of G2, the carrier of G2:] ) by XBOOLE_0:def 3;
[a,b] in the InternalRel of (union_of (G1,G2)) ` by ;
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 ;
per cases ( [a,b] in [: the carrier of G1, the carrier of G1:] or [a,b] in [: the carrier of (), the carrier of ():] or [a,b] in [: the carrier of (), the carrier of ():] or [a,b] in [: the carrier of G2, the carrier of G2:] ) by ;
suppose [a,b] in [: the carrier of G1, the carrier of G1:] ; :: thesis: [a,b] in the InternalRel of (sum_of ((),()))
then [a,b] in [: the carrier of G1, the carrier of G1:] \ the InternalRel of G1 by ;
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 ;
then [a,b] in the InternalRel of () by NECKLACE:def 8;
then [a,b] in the InternalRel of () \/ (( the InternalRel of () \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]) by XBOOLE_0:def 3;
then [a,b] in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_1:113;
hence [a,b] in the InternalRel of (sum_of ((),())) by NECKLA_2:def 3; :: thesis: verum
end;
suppose [a,b] in [: the carrier of (), the carrier of ():] ; :: thesis: [a,b] in the InternalRel of (sum_of ((),()))
then [a,b] in the InternalRel of () \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
then [a,b] in ( the InternalRel of () \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
then [a,b] in the InternalRel of () \/ (( the InternalRel of () \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]) by XBOOLE_0:def 3;
then [a,b] in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_1:113;
hence [a,b] in the InternalRel of (sum_of ((),())) by NECKLA_2:def 3; :: thesis: verum
end;
suppose [a,b] in [: the carrier of (), the carrier of ():] ; :: thesis: [a,b] in the InternalRel of (sum_of ((),()))
then [a,b] in [: the carrier of (), the carrier of ():] \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
then [a,b] in the InternalRel of () \/ ([: the carrier of (), the carrier of ():] \/ [: the carrier of (), the carrier of ():]) by XBOOLE_0:def 3;
then [a,b] in ( the InternalRel of () \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_1:4;
then [a,b] in the InternalRel of () \/ (( the InternalRel of () \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]) by XBOOLE_0:def 3;
then [a,b] in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_1:113;
hence [a,b] in the InternalRel of (sum_of ((),())) 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 ((),()))
then [a,b] in [: the carrier of G2, the carrier of G2:] \ the InternalRel of G2 by ;
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 ;
then [a,b] in the InternalRel of () by NECKLACE:def 8;
then [a,b] in the InternalRel of () \/ the InternalRel of () by XBOOLE_0:def 3;
then [a,b] in ( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
then [a,b] in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
hence [a,b] in the InternalRel of (sum_of ((),())) by NECKLA_2:def 3; :: thesis: verum
end;
end;
end;
assume [a,b] in the InternalRel of (sum_of ((),())) ; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))
then [a,b] in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] by NECKLA_2:def 3;
then ( [a,b] in ( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():] or [a,b] in [: the carrier of (), the carrier of ():] ) by XBOOLE_0:def 3;
then A12: ( [a,b] in the InternalRel of () \/ the InternalRel of () or [a,b] in [: the carrier of (), the carrier of ():] or [a,b] in [: the carrier of (), the carrier of ():] ) by XBOOLE_0:def 3;
per cases ( [a,b] in the InternalRel of () or [a,b] in the InternalRel of () or [a,b] in [: the carrier of (), the carrier of ():] or [a,b] in [: the carrier of (), the carrier of ():] ) by ;
suppose [a,b] in the InternalRel of () ; :: 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))
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 ;
then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by ;
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;
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:14;
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 ;
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 ;
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;
end;
end;
end;
[a,b] in [: the carrier of G1, the carrier of G1:] \/ [: the carrier of G1, the carrier of G2:] by ;
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 ;
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 ;
hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum
end;
suppose [a,b] in the InternalRel of () ; :: 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))
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 ;
then not [: the carrier of G1, the carrier of G1:] /\ [: the carrier of G2, the carrier of G2:] is empty by ;
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;
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:14;
per cases ( [a,b] in id the carrier of G2 or [a,b] in id the carrier of G1 ) by ;
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 ;
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;
end;
end;
[a,b] in [: the carrier of G2, the carrier of G1:] \/ [: the carrier of G2, the carrier of G2:] by ;
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 ;
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 ;
hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum
end;
suppose [a,b] in [: the carrier of (), the carrier of ():] ; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))
then A23: [a,b] in [: the carrier of G1, the carrier of ():] 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))
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 ;
suppose A27: [a,b] in the InternalRel of G1 ; :: thesis: contradiction
A28: b in the carrier of G2 by ;
b in the carrier of G1 by ;
then b in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: thesis: verum
end;
suppose A29: [a,b] in the InternalRel of G2 ; :: thesis: contradiction
A30: a in the carrier of G1 by ;
a in the carrier of G2 by ;
then a in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: 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:14;
per cases ( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 ) by ;
suppose A33: [a,b] in id the carrier of G1 ; :: thesis: contradiction
A34: b in the carrier of G2 by ;
b in the carrier of G1 by ;
then b in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: thesis: verum
end;
suppose A35: [a,b] in id the carrier of G2 ; :: thesis: contradiction
A36: a in the carrier of G1 by ;
a in the carrier of G2 by ;
then a in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: 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 ;
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 ;
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 ;
hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum
end;
suppose [a,b] in [: the carrier of (), the carrier of ():] ; :: thesis: [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2)))
then A37: [a,b] in [: the carrier of G2, the carrier of ():] 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))
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 ;
suppose A41: [a,b] in the InternalRel of G1 ; :: thesis: contradiction
A42: a in the carrier of G2 by ;
a in the carrier of G1 by ;
then a in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: thesis: verum
end;
suppose A43: [a,b] in the InternalRel of G2 ; :: thesis: contradiction
A44: b in the carrier of G1 by ;
b in the carrier of G2 by ;
then b in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: 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:14;
per cases ( [a,b] in id the carrier of G1 or [a,b] in id the carrier of G2 ) by ;
suppose A47: [a,b] in id the carrier of G1 ; :: thesis: contradiction
A48: a in the carrier of G2 by ;
a in the carrier of G1 by ;
then a in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: thesis: verum
end;
suppose A49: [a,b] in id the carrier of G2 ; :: thesis: contradiction
A50: b in the carrier of G1 by ;
b in the carrier of G2 by ;
then b in the carrier of G1 /\ the carrier of G2 by ;
hence contradiction by A2; :: 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 ;
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 ;
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 ;
hence [a,b] in the InternalRel of (ComplRelStr (union_of (G1,G2))) by NECKLACE:def 8; :: thesis: verum
end;
end;
end;
the carrier of (ComplRelStr (union_of (G1,G2))) = the carrier of (union_of (G1,G2)) by NECKLACE:def 8
.= the carrier of G1 \/ the carrier of G2 by NECKLA_2:def 2 ;
hence ComplRelStr (union_of (G1,G2)) = sum_of ((),()) by ; :: thesis: verum