let R be non empty symmetric irreflexive RelStr ; :: thesis: ( not 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 #) = union_of (G1,G2) ) )

set cR = the carrier of R;

set IR = the InternalRel of R;

assume not 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 #) = union_of (G1,G2) )

then consider x, y being set such that

A1: ( x in the carrier of R & y in the carrier of R ) and

x <> y and

A2: not the InternalRel of R reduces x,y ;

reconsider x = x, y = y as Element of R by A1;

set A1 = component x;

set A2 = the carrier of R \ (component x);

reconsider A2 = the carrier of R \ (component x) as Subset of R ;

set G1 = subrelstr (component x);

set G2 = subrelstr A2;

A3: the carrier of (subrelstr A2) = A2 by YELLOW_0:def 15;

the carrier of R c= (component x) \/ A2

A6: the carrier of (subrelstr (component x)) = component x by YELLOW_0:def 15;

then A7: the carrier of (subrelstr (component x)) misses the carrier of (subrelstr A2) by A3, XBOOLE_1:79;

A8: the InternalRel of (subrelstr (component x)) misses the InternalRel of (subrelstr A2)

the InternalRel of R = the InternalRel of R ~ by RELAT_2:13;

then not the InternalRel of R \/ ( the InternalRel of R ~) reduces x,y by A2;

then not x,y are_convertible_wrt the InternalRel of R by REWRITE1:def 4;

then not [x,y] in EqCl the InternalRel of R by MSUALG_6:41;

then not y in component x by Th29;

then A49: subrelstr A2 is non empty strict RelStr by A3, XBOOLE_0:def 5;

the carrier of R = the carrier of (union_of ((subrelstr (component x)),(subrelstr A2))) by A6, A3, A5, NECKLA_2:def 2;

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 #) = union_of (G1,G2) ) by A6, A7, A49, A48; :: thesis: verum

( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R, the InternalRel of R #) = union_of (G1,G2) ) )

set cR = the carrier of R;

set IR = the InternalRel of R;

assume not 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 #) = union_of (G1,G2) )

then consider x, y being set such that

A1: ( x in the carrier of R & y in the carrier of R ) and

x <> y and

A2: not the InternalRel of R reduces x,y ;

reconsider x = x, y = y as Element of R by A1;

set A1 = component x;

set A2 = the carrier of R \ (component x);

reconsider A2 = the carrier of R \ (component x) as Subset of R ;

set G1 = subrelstr (component x);

set G2 = subrelstr A2;

A3: the carrier of (subrelstr A2) = A2 by YELLOW_0:def 15;

the carrier of R c= (component x) \/ A2

proof

then A5:
the carrier of R = (component x) \/ A2
;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R or a in (component x) \/ A2 )

assume A4: a in the carrier of R ; :: thesis: a in (component x) \/ A2

assume not a in (component x) \/ A2 ; :: thesis: contradiction

then ( not a in component x & not a in A2 ) by XBOOLE_0:def 3;

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

end;assume A4: a in the carrier of R ; :: thesis: a in (component x) \/ A2

assume not a in (component x) \/ A2 ; :: thesis: contradiction

then ( not a in component x & not a in A2 ) by XBOOLE_0:def 3;

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

A6: the carrier of (subrelstr (component x)) = component x by YELLOW_0:def 15;

then A7: the carrier of (subrelstr (component x)) misses the carrier of (subrelstr A2) by A3, XBOOLE_1:79;

A8: the InternalRel of (subrelstr (component x)) misses the InternalRel of (subrelstr A2)

proof

A12:
the InternalRel of (subrelstr A2) = the InternalRel of R \ the InternalRel of (subrelstr (component x))
set IG1 = the InternalRel of (subrelstr (component x));

set IG2 = the InternalRel of (subrelstr A2);

assume not the InternalRel of (subrelstr (component x)) misses the InternalRel of (subrelstr A2) ; :: thesis: contradiction

then the InternalRel of (subrelstr (component x)) /\ the InternalRel of (subrelstr A2) <> {} ;

then consider a being object such that

A9: a in the InternalRel of (subrelstr (component x)) /\ the InternalRel of (subrelstr A2) by XBOOLE_0:def 1;

a in the InternalRel of (subrelstr (component x)) by A9, XBOOLE_0:def 4;

then consider c1, c2 being object such that

A10: a = [c1,c2] and

A11: c1 in component x and

c2 in component x by A6, RELSET_1:2;

ex g1, g2 being object st

( a = [g1,g2] & g1 in A2 & g2 in A2 ) by A3, A9, RELSET_1:2;

then c1 in A2 by A10, XTUPLE_0:1;

then c1 in (component x) /\ A2 by A11, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

end;set IG2 = the InternalRel of (subrelstr A2);

assume not the InternalRel of (subrelstr (component x)) misses the InternalRel of (subrelstr A2) ; :: thesis: contradiction

then the InternalRel of (subrelstr (component x)) /\ the InternalRel of (subrelstr A2) <> {} ;

then consider a being object such that

A9: a in the InternalRel of (subrelstr (component x)) /\ the InternalRel of (subrelstr A2) by XBOOLE_0:def 1;

a in the InternalRel of (subrelstr (component x)) by A9, XBOOLE_0:def 4;

then consider c1, c2 being object such that

A10: a = [c1,c2] and

A11: c1 in component x and

c2 in component x by A6, RELSET_1:2;

ex g1, g2 being object st

( a = [g1,g2] & g1 in A2 & g2 in A2 ) by A3, A9, RELSET_1:2;

then c1 in A2 by A10, XTUPLE_0:1;

then c1 in (component x) /\ A2 by A11, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

proof

the InternalRel of R = the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2)
set IG1 = the InternalRel of (subrelstr (component x));

set IG2 = the InternalRel of (subrelstr A2);

thus the InternalRel of (subrelstr A2) c= the InternalRel of R \ the InternalRel of (subrelstr (component x)) :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of R \ the InternalRel of (subrelstr (component x)) c= the InternalRel of (subrelstr A2)

assume A17: a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) ; :: thesis: a in the InternalRel of (subrelstr A2)

then A18: a in the InternalRel of R by XBOOLE_0:def 5;

A19: not a in the InternalRel of (subrelstr (component x)) by A17, XBOOLE_0:def 5;

consider c1, c2 being object such that

A20: a = [c1,c2] and

A21: ( c1 in the carrier of R & c2 in the carrier of R ) by A17, RELSET_1:2;

reconsider c1 = c1, c2 = c2 as Element of R by A21;

A22: c1 <= c2 by A18, A20, ORDERS_2:def 5;

end;set IG2 = the InternalRel of (subrelstr A2);

thus the InternalRel of (subrelstr A2) c= the InternalRel of R \ the InternalRel of (subrelstr (component x)) :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of R \ the InternalRel of (subrelstr (component x)) c= the InternalRel of (subrelstr A2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) or a in the InternalRel of (subrelstr A2) )
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 (component x)) )

assume A13: a in the InternalRel of (subrelstr A2) ; :: thesis: a in the InternalRel of R \ the InternalRel of (subrelstr (component x))

then consider g1, g2 being object such that

A14: a = [g1,g2] and

A15: ( g1 in A2 & g2 in A2 ) by A3, RELSET_1:2;

reconsider g1 = g1, g2 = g2 as Element of (subrelstr A2) by A15, YELLOW_0:def 15;

reconsider u1 = g1, u2 = g2 as Element of R by A15;

A16: not a in the InternalRel of (subrelstr (component x)) by A13, XBOOLE_0:def 4, A8;

g1 <= g2 by A13, A14, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

then a in the InternalRel of R by A14, ORDERS_2:def 5;

hence a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) by A16, XBOOLE_0:def 5; :: thesis: verum

end;assume A13: a in the InternalRel of (subrelstr A2) ; :: thesis: a in the InternalRel of R \ the InternalRel of (subrelstr (component x))

then consider g1, g2 being object such that

A14: a = [g1,g2] and

A15: ( g1 in A2 & g2 in A2 ) by A3, RELSET_1:2;

reconsider g1 = g1, g2 = g2 as Element of (subrelstr A2) by A15, YELLOW_0:def 15;

reconsider u1 = g1, u2 = g2 as Element of R by A15;

A16: not a in the InternalRel of (subrelstr (component x)) by A13, XBOOLE_0:def 4, A8;

g1 <= g2 by A13, A14, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

then a in the InternalRel of R by A14, ORDERS_2:def 5;

hence a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) by A16, XBOOLE_0:def 5; :: thesis: verum

assume A17: a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) ; :: thesis: a in the InternalRel of (subrelstr A2)

then A18: a in the InternalRel of R by XBOOLE_0:def 5;

A19: not a in the InternalRel of (subrelstr (component x)) by A17, XBOOLE_0:def 5;

consider c1, c2 being object such that

A20: a = [c1,c2] and

A21: ( c1 in the carrier of R & c2 in the carrier of R ) by A17, RELSET_1:2;

reconsider c1 = c1, c2 = c2 as Element of R by A21;

A22: c1 <= c2 by A18, A20, ORDERS_2:def 5;

per cases
( ( c1 in component x & c2 in component x ) or ( c1 in component x & c2 in A2 ) or ( c1 in A2 & c2 in component x ) or ( c1 in A2 & c2 in A2 ) )
by A5, XBOOLE_0:def 3;

end;

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

then reconsider d2 = c2 as Element of (subrelstr (component x)) by YELLOW_0:def 15;

reconsider d1 = c1 as Element of (subrelstr (component x)) by A23, YELLOW_0:def 15;

d1 <= d2 by A6, A22, YELLOW_0:60;

hence a in the InternalRel of (subrelstr A2) by A19, A20, ORDERS_2:def 5; :: thesis: verum

end;reconsider d1 = c1 as Element of (subrelstr (component x)) by A23, YELLOW_0:def 15;

d1 <= d2 by A6, A22, YELLOW_0:60;

hence a in the InternalRel of (subrelstr A2) by A19, A20, ORDERS_2:def 5; :: thesis: verum

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

A25:
[:(component x),A2:] misses the InternalRel of R

then a in [:(component x),A2:] /\ the InternalRel of R by A18, XBOOLE_0:def 4;

hence a in the InternalRel of (subrelstr A2) by A25; :: thesis: verum

end;proof

a in [:(component x),A2:]
by A20, A24, ZFMISC_1:def 2;
assume
not [:(component x),A2:] misses the InternalRel of R
; :: thesis: contradiction

then [:(component x),A2:] /\ the InternalRel of R <> {} ;

then consider b being object such that

A26: b in [:(component x),A2:] /\ the InternalRel of R by XBOOLE_0:def 1;

A27: b in the InternalRel of R by A26, XBOOLE_0:def 4;

b in [:(component x),A2:] by A26, XBOOLE_0:def 4;

then consider b1, b2 being object such that

A28: b1 in component x and

A29: b2 in A2 and

A30: b = [b1,b2] by ZFMISC_1:def 2;

reconsider b2 = b2 as Element of R by A29;

reconsider b1 = b1 as Element of R by A28;

( the InternalRel of R c= EqCl the InternalRel of R & [x,b1] in EqCl the InternalRel of R ) by A28, Th29, MSUALG_5:def 1;

then [x,b2] in EqCl the InternalRel of R by A27, A30, EQREL_1:7;

then b2 in component x by Th29;

then b2 in (component x) /\ A2 by A29, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

end;then [:(component x),A2:] /\ the InternalRel of R <> {} ;

then consider b being object such that

A26: b in [:(component x),A2:] /\ the InternalRel of R by XBOOLE_0:def 1;

A27: b in the InternalRel of R by A26, XBOOLE_0:def 4;

b in [:(component x),A2:] by A26, XBOOLE_0:def 4;

then consider b1, b2 being object such that

A28: b1 in component x and

A29: b2 in A2 and

A30: b = [b1,b2] by ZFMISC_1:def 2;

reconsider b2 = b2 as Element of R by A29;

reconsider b1 = b1 as Element of R by A28;

( the InternalRel of R c= EqCl the InternalRel of R & [x,b1] in EqCl the InternalRel of R ) by A28, Th29, MSUALG_5:def 1;

then [x,b2] in EqCl the InternalRel of R by A27, A30, EQREL_1:7;

then b2 in component x by Th29;

then b2 in (component x) /\ A2 by A29, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

then a in [:(component x),A2:] /\ the InternalRel of R by A18, XBOOLE_0:def 4;

hence a in the InternalRel of (subrelstr A2) by A25; :: thesis: verum

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

A32:
[:A2,(component x):] misses the InternalRel of R

then a in [:A2,(component x):] /\ the InternalRel of R by A18, XBOOLE_0:def 4;

hence a in the InternalRel of (subrelstr A2) by A32; :: thesis: verum

end;proof

a in [:A2,(component x):]
by A20, A31, ZFMISC_1:def 2;
assume
not [:A2,(component x):] misses the InternalRel of R
; :: thesis: contradiction

then [:A2,(component x):] /\ the InternalRel of R <> {} ;

then consider b being object such that

A33: b in [:A2,(component x):] /\ the InternalRel of R by XBOOLE_0:def 1;

b in [:A2,(component x):] by A33, XBOOLE_0:def 4;

then consider b1, b2 being object such that

A34: b1 in A2 and

A35: b2 in component x and

A36: b = [b1,b2] by ZFMISC_1:def 2;

reconsider b1 = b1 as Element of R by A34;

reconsider b2 = b2 as Element of R by A35;

A37: [x,b2] in EqCl the InternalRel of R by A35, Th29;

A38: the InternalRel of R c= EqCl the InternalRel of R by MSUALG_5:def 1;

b in the InternalRel of R by A33, XBOOLE_0:def 4;

then [b2,b1] in EqCl the InternalRel of R by A36, A38, EQREL_1:6;

then [x,b1] in EqCl the InternalRel of R by A37, EQREL_1:7;

then b1 in component x by Th29;

then b1 in (component x) /\ A2 by A34, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

end;then [:A2,(component x):] /\ the InternalRel of R <> {} ;

then consider b being object such that

A33: b in [:A2,(component x):] /\ the InternalRel of R by XBOOLE_0:def 1;

b in [:A2,(component x):] by A33, XBOOLE_0:def 4;

then consider b1, b2 being object such that

A34: b1 in A2 and

A35: b2 in component x and

A36: b = [b1,b2] by ZFMISC_1:def 2;

reconsider b1 = b1 as Element of R by A34;

reconsider b2 = b2 as Element of R by A35;

A37: [x,b2] in EqCl the InternalRel of R by A35, Th29;

A38: the InternalRel of R c= EqCl the InternalRel of R by MSUALG_5:def 1;

b in the InternalRel of R by A33, XBOOLE_0:def 4;

then [b2,b1] in EqCl the InternalRel of R by A36, A38, EQREL_1:6;

then [x,b1] in EqCl the InternalRel of R by A37, EQREL_1:7;

then b1 in component x by Th29;

then b1 in (component x) /\ A2 by A34, XBOOLE_0:def 4;

hence contradiction by A6, A3, A7; :: thesis: verum

then a in [:A2,(component x):] /\ the InternalRel of R by A18, XBOOLE_0:def 4;

hence a in the InternalRel of (subrelstr A2) by A32; :: thesis: verum

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

then reconsider d2 = c2 as Element of (subrelstr A2) by YELLOW_0:def 15;

reconsider d1 = c1 as Element of (subrelstr A2) by A39, YELLOW_0:def 15;

d1 <= d2 by A3, A22, A39, YELLOW_0:60;

hence a in the InternalRel of (subrelstr A2) by A20, ORDERS_2:def 5; :: thesis: verum

end;reconsider d1 = c1 as Element of (subrelstr A2) by A39, YELLOW_0:def 15;

d1 <= d2 by A3, A22, A39, YELLOW_0:60;

hence a in the InternalRel of (subrelstr A2) by A20, ORDERS_2:def 5; :: thesis: verum

proof

then A48:
the InternalRel of R = the InternalRel of (union_of ((subrelstr (component x)),(subrelstr A2)))
by NECKLA_2:def 2;
set IG1 = the InternalRel of (subrelstr (component x));

set IG2 = the InternalRel of (subrelstr A2);

thus the InternalRel of R c= the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) c= the InternalRel of R

assume A41: a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) ; :: thesis: a in the InternalRel of R

end;set IG2 = the InternalRel of (subrelstr A2);

thus the InternalRel of R c= the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) c= the InternalRel of R

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) or a in the InternalRel of R )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of R or a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) )

assume A40: a in the InternalRel of R ; :: thesis: a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2)

assume not a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) ; :: thesis: contradiction

then ( not a in the InternalRel of (subrelstr (component x)) & not a in the InternalRel of (subrelstr A2) ) by XBOOLE_0:def 3;

hence contradiction by A12, A40, XBOOLE_0:def 5; :: thesis: verum

end;assume A40: a in the InternalRel of R ; :: thesis: a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2)

assume not a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) ; :: thesis: contradiction

then ( not a in the InternalRel of (subrelstr (component x)) & not a in the InternalRel of (subrelstr A2) ) by XBOOLE_0:def 3;

hence contradiction by A12, A40, XBOOLE_0:def 5; :: thesis: verum

assume A41: a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) ; :: thesis: a in the InternalRel of R

per cases
( a in the InternalRel of (subrelstr (component x)) or a in the InternalRel of (subrelstr A2) )
by A41, XBOOLE_0:def 3;

end;

suppose A42:
a in the InternalRel of (subrelstr (component x))
; :: thesis: a in the InternalRel of R

then consider v, w being object such that

A43: a = [v,w] and

A44: ( v in component x & w in component x ) by A6, RELSET_1:2;

reconsider v = v, w = w as Element of (subrelstr (component x)) by A44, YELLOW_0:def 15;

reconsider u1 = v, u2 = w as Element of R by A44;

v <= w by A42, A43, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

hence a in the InternalRel of R by A43, ORDERS_2:def 5; :: thesis: verum

end;A43: a = [v,w] and

A44: ( v in component x & w in component x ) by A6, RELSET_1:2;

reconsider v = v, w = w as Element of (subrelstr (component x)) by A44, YELLOW_0:def 15;

reconsider u1 = v, u2 = w as Element of R by A44;

v <= w by A42, A43, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

hence a in the InternalRel of R by A43, ORDERS_2:def 5; :: thesis: verum

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

then consider v, w being object such that

A46: a = [v,w] and

A47: ( v in A2 & w in A2 ) by A3, RELSET_1:2;

reconsider v = v, w = w as Element of (subrelstr A2) by A47, YELLOW_0:def 15;

reconsider u1 = v, u2 = w as Element of R by A47;

v <= w by A45, A46, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

hence a in the InternalRel of R by A46, ORDERS_2:def 5; :: thesis: verum

end;A46: a = [v,w] and

A47: ( v in A2 & w in A2 ) by A3, RELSET_1:2;

reconsider v = v, w = w as Element of (subrelstr A2) by A47, YELLOW_0:def 15;

reconsider u1 = v, u2 = w as Element of R by A47;

v <= w by A45, A46, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

hence a in the InternalRel of R by A46, ORDERS_2:def 5; :: thesis: verum

the InternalRel of R = the InternalRel of R ~ by RELAT_2:13;

then not the InternalRel of R \/ ( the InternalRel of R ~) reduces x,y by A2;

then not x,y are_convertible_wrt the InternalRel of R by REWRITE1:def 4;

then not [x,y] in EqCl the InternalRel of R by MSUALG_6:41;

then not y in component x by Th29;

then A49: subrelstr A2 is non empty strict RelStr by A3, XBOOLE_0:def 5;

the carrier of R = the carrier of (union_of ((subrelstr (component x)),(subrelstr A2))) by A6, A3, A5, NECKLA_2:def 2;

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 #) = union_of (G1,G2) ) by A6, A7, A49, A48; :: thesis: verum