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 (ComplRelStr R);
set cCR = the carrier of (ComplRelStr R);
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 (ComplRelStr R) and
A2: y in the carrier of (ComplRelStr R) and
x <> y and
A3: not the InternalRel of (ComplRelStr R) reduces x,y ;
reconsider x = x, y = y as Element of (ComplRelStr R) by A1, A2;
set A1 = component x;
set A2 = the carrier of R \ (component x);
reconsider A1 = component x as Subset of R by NECKLACE:def 8;
the InternalRel of (ComplRelStr R) = the InternalRel of (ComplRelStr R) ~ by RELAT_2:13;
then not the InternalRel of (ComplRelStr R) \/ ( the InternalRel of (ComplRelStr R) ~) reduces x,y by A3;
then not x,y are_convertible_wrt the InternalRel of (ComplRelStr R) by REWRITE1:def 4;
then not [x,y] in EqCl the InternalRel of (ComplRelStr R) by MSUALG_6:41;
then A4: not y in A1 by Th29;
reconsider A2 = the carrier of R \ (component x) as Subset of R ;
set G1 = subrelstr A1;
set G2 = subrelstr A2;
A5: the carrier of (subrelstr A1) = A1 by YELLOW_0:def 15;
set IG1 = the InternalRel of (subrelstr A1);
set IG2 = the InternalRel of (subrelstr A2);
set G1G2 = [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):];
set G2G1 = [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):];
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 A8, XBOOLE_0:def 3;

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 (subrelstr A2) = A2 by YELLOW_0:def 15;
then A10: the carrier of (subrelstr A1) misses the carrier of (subrelstr A2) by A5, XBOOLE_1:79;
A11: the InternalRel of (subrelstr A1) misses the InternalRel of (subrelstr A2)

proof

assume not the InternalRel of (subrelstr A1) misses the InternalRel of (subrelstr A2) ; :: thesis: contradiction
then the InternalRel of (subrelstr A1) /\ the InternalRel of (subrelstr A2) <> {} ;
then consider a being object such that
A12: a in the InternalRel of (subrelstr A1) /\ the InternalRel of (subrelstr A2) by XBOOLE_0:def 1;
a in the InternalRel of (subrelstr A1) by A12, XBOOLE_0:def 4;
then consider c1, c2 being object such that
A13: a = [c1,c2] and
A14: c1 in A1 and
c2 in A1 by A5, RELSET_1:2;
ex g1, g2 being object st
( a = [g1,g2] & g1 in A2 & g2 in A2 ) by A9, A12, RELSET_1:2;
then c1 in A2 by A13, XTUPLE_0:1;
then c1 in A1 /\ A2 by A14, XBOOLE_0:def 4;
hence contradiction by A5, A9, A10; :: thesis: verum

end;

A15: the InternalRel of (subrelstr A2) = (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]

proof

thus the InternalRel of (subrelstr A2) c= (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] :: according to XBOOLE_0:def 10 :: thesis: (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] c= the InternalRel of (subrelstr A2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr A2) or a in (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] )
assume A16: a in the InternalRel of (subrelstr A2) ; :: thesis: a in (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]
then consider g1, g2 being object such that
A17: a = [g1,g2] and
A18: g1 in A2 and
A19: g2 in A2 by A9, RELSET_1:2;
reconsider g1 = g1, g2 = g2 as Element of (subrelstr A2) by A18, A19, YELLOW_0:def 15;
reconsider u1 = g1, u2 = g2 as Element of R by A18, A19;
A20: not a in the InternalRel of (subrelstr A1) by A16, XBOOLE_0:def 4, A11;
A21: not a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]

proof

assume a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ; :: thesis: contradiction
then g2 in A1 by A5, A17, ZFMISC_1:87;
then g2 in A1 /\ A2 by A19, XBOOLE_0:def 4;
hence contradiction by A5, A9, A10; :: thesis: verum

end;

A22: not a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]

proof

assume a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] ; :: thesis: contradiction
then g1 in A1 by A5, A17, ZFMISC_1:87;
then g1 in A1 /\ A2 by A18, XBOOLE_0:def 4;
hence contradiction by A5, A9, A10; :: thesis: verum

end;

g1 <= g2 by A16, A17, ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
then a in the InternalRel of R by A17, ORDERS_2:def 5;
then a in the InternalRel of R \ the InternalRel of (subrelstr A1) by A20, XBOOLE_0:def 5;
then a in ( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] by A22, XBOOLE_0:def 5;
hence a in (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] by A21, XBOOLE_0:def 5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] or a in the InternalRel of (subrelstr A2) )
assume A23: a in (( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ; :: thesis: a in the InternalRel of (subrelstr A2)
then A24: not a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] by XBOOLE_0:def 5;
A25: a in ( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] by A23, XBOOLE_0:def 5;
then A26: a in the InternalRel of R \ the InternalRel of (subrelstr A1) by XBOOLE_0:def 5;
then A27: not a in the InternalRel of (subrelstr A1) by XBOOLE_0:def 5;
A28: not a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] by A25, XBOOLE_0:def 5;
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 A23, RELSET_1:2;
reconsider c1 = c1, c2 = c2 as Element of R by A30;
a in the InternalRel of R by A26, XBOOLE_0:def 5;
then A31: c1 <= c2 by A29, ORDERS_2:def 5;

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 A6, XBOOLE_0:def 3;

suppose A32: ( c1 in A1 & c2 in A1 ) ; :: thesis: a in the InternalRel of (subrelstr A2)

then reconsider d2 = c2 as Element of (subrelstr A1) by YELLOW_0:def 15;
reconsider d1 = c1 as Element of (subrelstr A1) by A32, YELLOW_0:def 15;
d1 <= d2 by A5, A31, YELLOW_0:60;
hence a in the InternalRel of (subrelstr A2) by A27, A29, ORDERS_2:def 5; :: thesis: verum

end;

suppose ( c1 in A1 & c2 in A2 ) ; :: thesis: a in the InternalRel of (subrelstr A2)

hence a in the InternalRel of (subrelstr A2) by A5, A9, A28, A29, ZFMISC_1:87; :: thesis: verum

end;

suppose ( c1 in A2 & c2 in A1 ) ; :: thesis: a in the InternalRel of (subrelstr A2)

hence a in the InternalRel of (subrelstr A2) by A5, A9, A24, A29, ZFMISC_1:87; :: thesis: verum

end;

suppose A33: ( c1 in A2 & c2 in A2 ) ; :: thesis: a in the InternalRel of (subrelstr A2)

then reconsider d1 = c1, d2 = c2 as Element of (subrelstr A2) by YELLOW_0:def 15;
d1 <= d2 by A9, A31, A33, YELLOW_0:60;
hence a in the InternalRel of (subrelstr A2) by A29, ORDERS_2:def 5; :: thesis: verum

end;

end;

end;

the InternalRel of R = (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]

proof

set G1G2 = [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):];
set G2G1 = [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):];
thus the InternalRel of R c= (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] :: according to XBOOLE_0:def 10 :: thesis: (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] 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 (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] )
assume A34: a in the InternalRel of R ; :: thesis: a in (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]
assume A35: not a in (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ; :: thesis: contradiction
then A36: not a in ( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] by XBOOLE_0:def 3;
then A37: not a in the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2) by XBOOLE_0:def 3;
then not a in the InternalRel of (subrelstr A2) by XBOOLE_0:def 3;
then ( not a in ( the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] or a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ) by A15, XBOOLE_0:def 5;
then A38: ( not a in the InternalRel of R \ the InternalRel of (subrelstr A1) or a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] or a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ) by XBOOLE_0:def 5;
not a in the InternalRel of (subrelstr A1) by A37, XBOOLE_0:def 3;
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 (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] or a in the InternalRel of R )
assume a in (( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]) \/ [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ; :: thesis: a in the InternalRel of R
then ( a in ( the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] or a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ) by XBOOLE_0:def 3;
then A39: ( a in the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2) or a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] or a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ) by XBOOLE_0:def 3;

per cases ( a in the InternalRel of (subrelstr A1) or a in the InternalRel of (subrelstr A2) or a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] or a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ) by A39, XBOOLE_0:def 3;

suppose A40: a in the InternalRel of (subrelstr A1) ; :: 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 A5, RELSET_1:2;
reconsider v = v, w = w as Element of (subrelstr A1) by A42, YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A42;
v <= w by A40, A41, ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by A41, ORDERS_2:def 5; :: thesis: verum

end;

suppose A43: a in the InternalRel of (subrelstr A2) ; :: 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 A9, RELSET_1:2;
reconsider v = v, w = w as Element of (subrelstr A2) by A45, YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A45;
v <= w by A43, A44, ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by A44, ORDERS_2:def 5; :: thesis: verum

end;

suppose A46: a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):] ; :: 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 A46, RELAT_1:def 1;
A49: w in A2 by A9, A46, A48, ZFMISC_1:87;
A50: v in A1 by A5, A46, A48, ZFMISC_1:87;
then reconsider v = v, w = w as Element of (ComplRelStr R) by A49, NECKLACE:def 8;
v <> w by A5, A9, A10, A50, A49, XBOOLE_0:def 4;
then A51: not a in id the carrier of R by A48, RELAT_1:def 10;
[v,w] in [: the carrier of R, the carrier of R:] by A50, A49, ZFMISC_1:87;
then a in [: the carrier of R, the carrier of R:] \ the InternalRel of R by A48, A47, XBOOLE_0:def 5;
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 A51, XBOOLE_0:def 5;
then [v,w] in the InternalRel of (ComplRelStr R) by A48, NECKLACE:def 8;
then v,w are_convertible_wrt the InternalRel of (ComplRelStr R) by REWRITE1:29;
then A52: [v,w] in EqCl the InternalRel of (ComplRelStr R) by MSUALG_6:41;
[x,v] in EqCl the InternalRel of (ComplRelStr R) by A50, Th29;
then [x,w] in EqCl the InternalRel of (ComplRelStr R) by A52, EQREL_1:7;
then w in component x by Th29;
then w in A1 /\ A2 by A49, XBOOLE_0:def 4;
hence contradiction by A5, A9, A10; :: thesis: verum

end;

suppose A53: a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):] ; :: 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 A53, RELAT_1:def 1;
A56: w in A1 by A5, A53, A55, ZFMISC_1:87;
A57: v in A2 by A9, A53, A55, ZFMISC_1:87;
then reconsider v = v, w = w as Element of (ComplRelStr R) by A56, NECKLACE:def 8;
v <> w by A5, A9, A10, A57, A56, XBOOLE_0:def 4;
then A58: not a in id the carrier of R by A55, RELAT_1:def 10;
[v,w] in [: the carrier of R, the carrier of R:] by A57, A56, ZFMISC_1:87;
then a in [: the carrier of R, the carrier of R:] \ the InternalRel of R by A55, A54, XBOOLE_0:def 5;
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 A58, XBOOLE_0:def 5;
then [v,w] in the InternalRel of (ComplRelStr R) by A55, NECKLACE:def 8;
then v,w are_convertible_wrt the InternalRel of (ComplRelStr R) by REWRITE1:29;
then [v,w] in EqCl the InternalRel of (ComplRelStr R) by MSUALG_6:41;
then A59: [w,v] in EqCl the InternalRel of (ComplRelStr R) by EQREL_1:6;
[x,w] in EqCl the InternalRel of (ComplRelStr R) by A56, Th29;
then [x,v] in EqCl the InternalRel of (ComplRelStr R) by A59, EQREL_1:7;
then v in component x by Th29;
then v in A1 /\ A2 by A57, XBOOLE_0:def 4;
hence contradiction by A5, A9, A10; :: thesis: verum

end;

end;

end;

then A60: the InternalRel of R = the InternalRel of (sum_of ((subrelstr A1),(subrelstr A2))) by NECKLA_2:def 3;
y in the carrier of R by A2, NECKLACE:def 8;
then A61: subrelstr A2 is non empty strict RelStr by A9, A4, XBOOLE_0:def 5;
the carrier of R = the carrier of (sum_of ((subrelstr A1),(subrelstr A2))) by A5, A9, A6, NECKLA_2:def 3;
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