let R be non empty symmetric irreflexive RelStr ; :: thesis:
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:
then consider x, y being set such that
A1: ( x in the carrier of (ComplRelStr R) & y in the carrier of (ComplRelStr R) & x <> y & not the InternalRel of (ComplRelStr R) reduces x,y ) by Def2;
reconsider x = x, y = y as Element of (ComplRelStr R) by A1;
set A1 = component x;
set A2 = the carrier of R \ (component x);
reconsider A1 = component x as Subset of R by NECKLACE:def 9;
reconsider A2 = the carrier of R \ (component x) as Subset of R ;
set G1 = subrelstr A1;
set G2 = subrelstr A2;
A2: ( the carrier of (subrelstr A1) = A1 & the carrier of (subrelstr A2) = A2 ) by YELLOW_0:def 15;
then A3: the carrier of (subrelstr A1) misses the carrier of (subrelstr A2) by XBOOLE_1:79;
the InternalRel of (ComplRelStr R) = the InternalRel of (ComplRelStr R) ~ by RELAT_2:30;
then not the InternalRel of (ComplRelStr R) \/ (the InternalRel of (ComplRelStr R) ~ ) reduces x,y by A1;
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 ( y in the carrier of R & not y in A1 ) by A1, Th30, NECKLACE:def 9;
then not the carrier of (subrelstr A2) is empty by A2, XBOOLE_0:def 5;
then A4: ( subrelstr A1 is non empty strict RelStr & subrelstr A2 is non empty strict RelStr ) by A2;
A5: the carrier of R = A1 \/ A2

proof

thus the carrier of R c= A1 \/ A2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: a in the carrier of R ; :: thesis:
assume not a in A1 \/ A2 ; :: thesis:
then ( not a in A1 & not a in A2 ) by XBOOLE_0:def 3;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: a in A1 \/ A2 ; :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose a in A1 ; :: thesis:

hence a in the carrier of R ; :: thesis:

end;

suppose a in A2 ; :: thesis:

hence a in the carrier of R ; :: thesis:

end;

then A8: the carrier of R = the carrier of (sum_of (subrelstr A1),(subrelstr A2)) by A2, NECKLA_2:def 3;
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):];
A9: 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:
then the InternalRel of (subrelstr A1) /\ the InternalRel of (subrelstr A2) <> {} by XBOOLE_0:def 7;
then consider a being set such that
A10: a in the InternalRel of (subrelstr A1) /\ the InternalRel of (subrelstr A2) by XBOOLE_0:def 1;
A11: ( a in the InternalRel of (subrelstr A1) & a in the InternalRel of (subrelstr A2) ) by A10, XBOOLE_0:def 4;
then consider c1, c2 being set such that
A12: ( a = [c1,c2] & c1 in A1 & c2 in A1 ) by A2, RELSET_1:6;
consider g1, g2 being set such that
A13: ( a = [g1,g2] & g1 in A2 & g2 in A2 ) by A2, A11, RELSET_1:6;
( c1 in A1 & c1 in A2 ) by A12, A13, ZFMISC_1:33;
then c1 in A1 /\ A2 by XBOOLE_0:def 4;
hence contradiction by A2, A3, XBOOLE_0:def 7; :: thesis:

end;

A14: 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:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: a in the InternalRel of (subrelstr A2) ; :: thesis:
then consider g1, g2 being set such that
A16: ( a = [g1,g2] & g1 in A2 & g2 in A2 ) by A2, RELSET_1:6;
reconsider g1 = g1, g2 = g2 as Element of (subrelstr A2) by A16, YELLOW_0:def 15;
A17: g1 <= g2 by A15, A16, ORDERS_2:def 9;
reconsider u1 = g1, u2 = g2 as Element of R by A16;
u1 <= u2 by A17, YELLOW_0:60;
then A18: a in the InternalRel of R by A16, ORDERS_2:def 9;
A19: not a in the InternalRel of (subrelstr A1)

proof

assume a in the InternalRel of (subrelstr A1) ; :: thesis:
then a in the InternalRel of (subrelstr A1) /\ the InternalRel of (subrelstr A2) by A15, XBOOLE_0:def 4;
hence contradiction by A9, XBOOLE_0:def 7; :: thesis:

end;

A20: 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:
then ( g1 in A1 & g2 in A2 ) by A2, A16, ZFMISC_1:106;
then g1 in A1 /\ A2 by A16, XBOOLE_0:def 4;
hence contradiction by A2, A3, XBOOLE_0:def 7; :: thesis:

end;

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:
then ( g1 in A2 & g2 in A1 ) by A2, A16, ZFMISC_1:106;
then g2 in A1 /\ A2 by A16, XBOOLE_0:def 4;
hence contradiction by A2, A3, XBOOLE_0:def 7; :: thesis:

end;

a in the InternalRel of R \ the InternalRel of (subrelstr A1) by A18, A19, 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 A20, 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:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume 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:
then A22: ( a in (the InternalRel of R \ the InternalRel of (subrelstr A1)) \ [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) by XBOOLE_0:def 5;
then A23: ( a in the InternalRel of R \ the InternalRel of (subrelstr A1) & not a in [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) by XBOOLE_0:def 5;
then A24: ( a in the InternalRel of R & not a in the InternalRel of (subrelstr A1) & not a in [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) by XBOOLE_0:def 5;
then consider c1, c2 being set such that
A25: ( a = [c1,c2] & c1 in the carrier of R & c2 in the carrier of R ) by RELSET_1:6;
reconsider c1 = c1, c2 = c2 as Element of R by A25;
A26: c1 <= c2 by A24, A25, ORDERS_2:def 9;

per cases by A5, XBOOLE_0:def 3;

suppose A27: ( c1 in A1 & c2 in A1 ) ; :: thesis:

then reconsider d1 = c1 as Element of (subrelstr A1) by YELLOW_0:def 15;
reconsider d2 = c2 as Element of (subrelstr A1) by A27, YELLOW_0:def 15;
d1 <= d2 by A2, A26, YELLOW_0:61;
hence a in the InternalRel of (subrelstr A2) by A24, A25, ORDERS_2:def 9; :: thesis:

end;

suppose ( c1 in A1 & c2 in A2 ) ; :: thesis:

hence a in the InternalRel of (subrelstr A2) by A2, A23, A25, ZFMISC_1:106; :: thesis:

end;

suppose ( c1 in A2 & c2 in A1 ) ; :: thesis:

hence a in the InternalRel of (subrelstr A2) by A2, A22, A25, ZFMISC_1:106; :: thesis:

end;

suppose A28: ( c1 in A2 & c2 in A2 ) ; :: thesis:

then reconsider d1 = c1, d2 = c2 as Element of (subrelstr A2) by YELLOW_0:def 15;
d1 <= d2 by A2, A26, A28, YELLOW_0:61;
hence a in the InternalRel of (subrelstr A2) by A25, ORDERS_2:def 9; :: thesis:

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:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: a in the InternalRel of R ; :: thesis:
assume 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:
then ( not a in (the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2)) \/ [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) by XBOOLE_0:def 3;
then ( not a in the InternalRel of (subrelstr A1) \/ the InternalRel of (subrelstr A2) & not a in [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) by XBOOLE_0:def 3;
then A30: ( not a in the InternalRel of (subrelstr A1) & not a in the InternalRel of (subrelstr A2) & not a in [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] & not a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ) 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 A14, XBOOLE_0:def 5;
then ( 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;
hence contradiction by A29, A30, XBOOLE_0:def 5; :: thesis:

end;

per cases by A32, XBOOLE_0:def 3;

suppose A33: a in the InternalRel of (subrelstr A1) ; :: thesis:

then consider v, w being set such that
A34: ( a = [v,w] & v in A1 & w in A1 ) by A2, RELSET_1:6;
reconsider v = v, w = w as Element of (subrelstr A1) by A34, YELLOW_0:def 15;
A35: v <= w by A33, A34, ORDERS_2:def 9;
reconsider u1 = v, u2 = w as Element of R by A34;
u1 <= u2 by A35, YELLOW_0:60;
hence a in the InternalRel of R by A34, ORDERS_2:def 9; :: thesis:

end;

suppose A36: a in the InternalRel of (subrelstr A2) ; :: thesis:

then consider v, w being set such that
A37: ( a = [v,w] & v in A2 & w in A2 ) by A2, RELSET_1:6;
reconsider v = v, w = w as Element of (subrelstr A2) by A37, YELLOW_0:def 15;
A38: v <= w by A36, A37, ORDERS_2:def 9;
reconsider u1 = v, u2 = w as Element of R by A37;
u1 <= u2 by A38, YELLOW_0:60;
hence a in the InternalRel of R by A37, ORDERS_2:def 9; :: thesis:

end;

suppose A39: a in [:the carrier of (subrelstr A1),the carrier of (subrelstr A2):] ; :: thesis:

then consider v, w being set such that
A40: a = [v,w] by RELAT_1:def 1;
A41: ( v in A1 & w in A2 ) by A2, A39, A40, ZFMISC_1:106;
then reconsider v = v, w = w as Element of (ComplRelStr R) by NECKLACE:def 9;
A42: v <> w

proof

assume A43: v = w ; :: thesis:
A1 /\ A2 = {} by A2, A3, XBOOLE_0:def 7;
hence contradiction by A41, A43, XBOOLE_0:def 4; :: thesis:

end;

assume A44: not a in the InternalRel of R ; :: thesis:
A45: not a in id the carrier of R by A40, A42, RELAT_1:def 10;
[v,w] in [:the carrier of R,the carrier of R:] by A41, ZFMISC_1:106;
then a in [:the carrier of R,the carrier of R:] \ the InternalRel of R by A40, A44, XBOOLE_0:def 5;
then a in the InternalRel of R ` by SUBSET_1:def 5;
then a in (the InternalRel of R ` ) \ (id the carrier of R) by A45, XBOOLE_0:def 5;
then [v,w] in the InternalRel of (ComplRelStr R) by A40, NECKLACE:def 9;
then v,w are_convertible_wrt the InternalRel of (ComplRelStr R) by REWRITE1:30;
then A46: [v,w] in EqCl the InternalRel of (ComplRelStr R) by MSUALG_6:41;
[x,v] in EqCl the InternalRel of (ComplRelStr R) by A41, Th30;
then [x,w] in EqCl the InternalRel of (ComplRelStr R) by A46, EQREL_1:13;
then w in component x by Th30;
then w in A1 /\ A2 by A41, XBOOLE_0:def 4;
hence contradiction by A2, A3, XBOOLE_0:def 7; :: thesis:

end;

suppose A47: a in [:the carrier of (subrelstr A2),the carrier of (subrelstr A1):] ; :: thesis:

then consider v, w being set such that
A48: a = [v,w] by RELAT_1:def 1;
A49: ( v in A2 & w in A1 ) by A2, A47, A48, ZFMISC_1:106;
then reconsider v = v, w = w as Element of (ComplRelStr R) by NECKLACE:def 9;
A50: v <> w

proof

assume A51: v = w ; :: thesis:
A1 /\ A2 = {} by A2, A3, XBOOLE_0:def 7;
hence contradiction by A49, A51, XBOOLE_0:def 4; :: thesis:

end;

assume A52: not a in the InternalRel of R ; :: thesis:
A53: not a in id the carrier of R by A48, A50, RELAT_1:def 10;
[v,w] in [:the carrier of R,the carrier of R:] by A49, ZFMISC_1:106;
then a in [:the carrier of R,the carrier of R:] \ the InternalRel of R by A48, A52, XBOOLE_0:def 5;
then a in the InternalRel of R ` by SUBSET_1:def 5;
then a in (the InternalRel of R ` ) \ (id the carrier of R) by A53, XBOOLE_0:def 5;
then [v,w] in the InternalRel of (ComplRelStr R) by A48, NECKLACE:def 9;
then v,w are_convertible_wrt the InternalRel of (ComplRelStr R) by REWRITE1:30;
then [v,w] in EqCl the InternalRel of (ComplRelStr R) by MSUALG_6:41;
then A54: [w,v] in EqCl the InternalRel of (ComplRelStr R) by EQREL_1:12;
[x,w] in EqCl the InternalRel of (ComplRelStr R) by A49, Th30;
then [x,v] in EqCl the InternalRel of (ComplRelStr R) by A54, EQREL_1:13;
then v in component x by Th30;
then v in A1 /\ A2 by A49, XBOOLE_0:def 4;
hence contradiction by A2, A3, XBOOLE_0:def 7; :: thesis:

end;

then the InternalRel of R = the InternalRel of (sum_of (subrelstr A1),(subrelstr A2)) by 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 A3, A4, A8; :: thesis: