let R be non empty symmetric irreflexive RelStr ; :: thesis: ( not ComplRelStr R is path-connected implies ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) ) )

set cR = the carrier of R;
set IR = the InternalRel of R;
set CR = ComplRelStr R;
set ICR = the InternalRel of ();
set cCR = the carrier of ();
assume not ComplRelStr R is path-connected ; :: thesis: ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) )

then consider x, y being set such that
A1: x in the carrier of () and
A2: y in the carrier of () and
x <> y and
A3: not the InternalRel of () reduces x,y ;
reconsider x = x, y = y as Element of () by A1, A2;
set A1 = component x;
set A2 = the carrier of R \ ();
reconsider A1 = component x as Subset of R by NECKLACE:def 8;
the InternalRel of () = the InternalRel of () ~ by RELAT_2:13;
then not the InternalRel of () \/ ( the InternalRel of () ~) reduces x,y by A3;
then not x,y are_convertible_wrt the InternalRel of () by REWRITE1:def 4;
then not [x,y] in EqCl the InternalRel of () by MSUALG_6:41;
then A4: not y in A1 by Th29;
reconsider A2 = the carrier of R \ () as Subset of R ;
set G1 = subrelstr A1;
set G2 = subrelstr A2;
A5: the carrier of () = A1 by YELLOW_0:def 15;
set IG1 = the InternalRel of ();
set IG2 = the InternalRel of ();
set G1G2 = [: the carrier of (), the carrier of ():];
set G2G1 = [: the carrier of (), the carrier of ():];
A6: the carrier of R = A1 \/ A2
proof
thus the carrier of R c= A1 \/ A2 :: according to XBOOLE_0:def 10 :: thesis: A1 \/ A2 c= the carrier of R
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R or a in A1 \/ A2 )
assume A7: a in the carrier of R ; :: thesis: a in A1 \/ A2
assume not a in A1 \/ A2 ; :: thesis: contradiction
then ( not a in A1 & not a in A2 ) by XBOOLE_0:def 3;
hence contradiction by A7, XBOOLE_0:def 5; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 \/ A2 or a in the carrier of R )
assume A8: a in A1 \/ A2 ; :: thesis: a in the carrier of R
per cases ( a in A1 or a in A2 ) by ;
suppose a in A1 ; :: thesis: a in the carrier of R
hence a in the carrier of R ; :: thesis: verum
end;
suppose a in A2 ; :: thesis: a in the carrier of R
hence a in the carrier of R ; :: thesis: verum
end;
end;
end;
A9: the carrier of () = A2 by YELLOW_0:def 15;
then A10: the carrier of () misses the carrier of () by ;
A11: the InternalRel of () misses the InternalRel of ()
proof
assume not the InternalRel of () misses the InternalRel of () ; :: thesis: contradiction
then the InternalRel of () /\ the InternalRel of () <> {} ;
then consider a being object such that
A12: a in the InternalRel of () /\ the InternalRel of () by XBOOLE_0:def 1;
a in the InternalRel of () by ;
then consider c1, c2 being object such that
A13: a = [c1,c2] and
A14: c1 in A1 and
c2 in A1 by ;
ex g1, g2 being object st
( a = [g1,g2] & g1 in A2 & g2 in A2 ) by ;
then c1 in A2 by ;
then c1 in A1 /\ A2 by ;
hence contradiction by A5, A9, A10; :: thesis: verum
end;
A15: the InternalRel of () = (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():]
proof
thus the InternalRel of () c= (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] :: according to XBOOLE_0:def 10 :: thesis: (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] c= the InternalRel of ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of () or a in (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] )
assume A16: a in the InternalRel of () ; :: thesis: a in (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():]
then consider g1, g2 being object such that
A17: a = [g1,g2] and
A18: g1 in A2 and
A19: g2 in A2 by ;
reconsider g1 = g1, g2 = g2 as Element of () by ;
reconsider u1 = g1, u2 = g2 as Element of R by ;
A20: not a in the InternalRel of () by ;
A21: not a in [: the carrier of (), the carrier of ():]
proof
assume a in [: the carrier of (), the carrier of ():] ; :: thesis: contradiction
then g2 in A1 by ;
then g2 in A1 /\ A2 by ;
hence contradiction by A5, A9, A10; :: thesis: verum
end;
A22: not a in [: the carrier of (), the carrier of ():]
proof
assume a in [: the carrier of (), the carrier of ():] ; :: thesis: contradiction
then g1 in A1 by ;
then g1 in A1 /\ A2 by ;
hence contradiction by A5, A9, A10; :: thesis: verum
end;
g1 <= g2 by ;
then u1 <= u2 by YELLOW_0:59;
then a in the InternalRel of R by ;
then a in the InternalRel of R \ the InternalRel of () by ;
then a in ( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():] by ;
hence a in (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] by ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] or a in the InternalRel of () )
assume A23: a in (( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():]) \ [: the carrier of (), the carrier of ():] ; :: thesis: a in the InternalRel of ()
then A24: not a in [: the carrier of (), the carrier of ():] by XBOOLE_0:def 5;
A25: a in ( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():] by ;
then A26: a in the InternalRel of R \ the InternalRel of () by XBOOLE_0:def 5;
then A27: not a in the InternalRel of () by XBOOLE_0:def 5;
A28: not a in [: the carrier of (), the carrier of ():] by ;
consider c1, c2 being object such that
A29: a = [c1,c2] and
A30: ( c1 in the carrier of R & c2 in the carrier of R ) by ;
reconsider c1 = c1, c2 = c2 as Element of R by A30;
a in the InternalRel of R by ;
then A31: c1 <= c2 by ;
per cases ( ( c1 in A1 & c2 in A1 ) or ( c1 in A1 & c2 in A2 ) or ( c1 in A2 & c2 in A1 ) or ( c1 in A2 & c2 in A2 ) ) by ;
suppose A32: ( c1 in A1 & c2 in A1 ) ; :: thesis: a in the InternalRel of ()
then reconsider d2 = c2 as Element of () by YELLOW_0:def 15;
reconsider d1 = c1 as Element of () by ;
d1 <= d2 by ;
hence a in the InternalRel of () by ; :: thesis: verum
end;
suppose ( c1 in A1 & c2 in A2 ) ; :: thesis: a in the InternalRel of ()
hence a in the InternalRel of () by ; :: thesis: verum
end;
suppose ( c1 in A2 & c2 in A1 ) ; :: thesis: a in the InternalRel of ()
hence a in the InternalRel of () by ; :: thesis: verum
end;
suppose A33: ( c1 in A2 & c2 in A2 ) ; :: thesis: a in the InternalRel of ()
then reconsider d1 = c1, d2 = c2 as Element of () by YELLOW_0:def 15;
d1 <= d2 by ;
hence a in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
the InternalRel of R = (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]
proof
set G1G2 = [: the carrier of (), the carrier of ():];
set G2G1 = [: the carrier of (), the carrier of ():];
thus the InternalRel of R c= (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] :: according to XBOOLE_0:def 10 :: thesis: (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] c= the InternalRel of R
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of R or a in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] )
assume A34: a in the InternalRel of R ; :: thesis: a in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():]
assume A35: not a in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] ; :: thesis: contradiction
then A36: not a in ( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():] by XBOOLE_0:def 3;
then A37: not a in the InternalRel of () \/ the InternalRel of () by XBOOLE_0:def 3;
then not a in the InternalRel of () by XBOOLE_0:def 3;
then ( not a in ( the InternalRel of R \ the InternalRel of ()) \ [: the carrier of (), the carrier of ():] or a in [: the carrier of (), the carrier of ():] ) by ;
then A38: ( not a in the InternalRel of R \ the InternalRel of () or a in [: the carrier of (), the carrier of ():] or a in [: the carrier of (), the carrier of ():] ) by XBOOLE_0:def 5;
not a in the InternalRel of () by ;
hence contradiction by A34, A35, A36, A38, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] or a in the InternalRel of R )
assume a in (( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():]) \/ [: the carrier of (), the carrier of ():] ; :: thesis: a in the InternalRel of R
then ( a in ( the InternalRel of () \/ the InternalRel of ()) \/ [: the carrier of (), the carrier of ():] or a in [: the carrier of (), the carrier of ():] ) by XBOOLE_0:def 3;
then A39: ( a in the InternalRel of () \/ the InternalRel of () or a in [: the carrier of (), the carrier of ():] or a in [: the carrier of (), the carrier of ():] ) by XBOOLE_0:def 3;
per cases ( a in the InternalRel of () or a in the InternalRel of () or a in [: the carrier of (), the carrier of ():] or a in [: the carrier of (), the carrier of ():] ) by ;
suppose A40: a in the InternalRel of () ; :: thesis: a in the InternalRel of R
then consider v, w being object such that
A41: a = [v,w] and
A42: ( v in A1 & w in A1 ) by ;
reconsider v = v, w = w as Element of () by ;
reconsider u1 = v, u2 = w as Element of R by A42;
v <= w by ;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by ; :: thesis: verum
end;
suppose A43: a in the InternalRel of () ; :: thesis: a in the InternalRel of R
then consider v, w being object such that
A44: a = [v,w] and
A45: ( v in A2 & w in A2 ) by ;
reconsider v = v, w = w as Element of () by ;
reconsider u1 = v, u2 = w as Element of R by A45;
v <= w by ;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by ; :: thesis: verum
end;
suppose A46: a in [: the carrier of (), the carrier of ():] ; :: thesis: a in the InternalRel of R
assume A47: not a in the InternalRel of R ; :: thesis: contradiction
consider v, w being object such that
A48: a = [v,w] by ;
A49: w in A2 by ;
A50: v in A1 by ;
then reconsider v = v, w = w as Element of () by ;
v <> w by ;
then A51: not a in id the carrier of R by ;
[v,w] in [: the carrier of R, the carrier of R:] by ;
then a in [: the carrier of R, the carrier of R:] \ the InternalRel of R by ;
then a in the InternalRel of R ` by SUBSET_1:def 4;
then a in ( the InternalRel of R `) \ (id the carrier of R) by ;
then [v,w] in the InternalRel of () by ;
then v,w are_convertible_wrt the InternalRel of () by REWRITE1:29;
then A52: [v,w] in EqCl the InternalRel of () by MSUALG_6:41;
[x,v] in EqCl the InternalRel of () by ;
then [x,w] in EqCl the InternalRel of () by ;
then w in component x by Th29;
then w in A1 /\ A2 by ;
hence contradiction by A5, A9, A10; :: thesis: verum
end;
suppose A53: a in [: the carrier of (), the carrier of ():] ; :: thesis: a in the InternalRel of R
assume A54: not a in the InternalRel of R ; :: thesis: contradiction
consider v, w being object such that
A55: a = [v,w] by ;
A56: w in A1 by ;
A57: v in A2 by ;
then reconsider v = v, w = w as Element of () by ;
v <> w by ;
then A58: not a in id the carrier of R by ;
[v,w] in [: the carrier of R, the carrier of R:] by ;
then a in [: the carrier of R, the carrier of R:] \ the InternalRel of R by ;
then a in the InternalRel of R ` by SUBSET_1:def 4;
then a in ( the InternalRel of R `) \ (id the carrier of R) by ;
then [v,w] in the InternalRel of () by ;
then v,w are_convertible_wrt the InternalRel of () by REWRITE1:29;
then [v,w] in EqCl the InternalRel of () by MSUALG_6:41;
then A59: [w,v] in EqCl the InternalRel of () by EQREL_1:6;
[x,w] in EqCl the InternalRel of () by ;
then [x,v] in EqCl the InternalRel of () by ;
then v in component x by Th29;
then v in A1 /\ A2 by ;
hence contradiction by A5, A9, A10; :: thesis: verum
end;
end;
end;
then A60: the InternalRel of R = the InternalRel of (sum_of ((),())) by NECKLA_2:def 3;
y in the carrier of R by ;
then A61: subrelstr A2 is non empty strict RelStr by ;
the carrier of R = the carrier of (sum_of ((),())) by ;
hence ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) ) by A5, A10, A61, A60; :: thesis: verum