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 \ ();
reconsider A2 = the carrier of R \ () as Subset of R ;
set G1 = subrelstr ();
set G2 = subrelstr A2;
A3: the carrier of () = A2 by YELLOW_0:def 15;
the carrier of R c= () \/ A2
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R or a in () \/ A2 )
assume A4: a in the carrier of R ; :: thesis: a in () \/ A2
assume not a in () \/ 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;
then A5: the carrier of R = () \/ A2 ;
A6: the carrier of () = component x by YELLOW_0:def 15;
then A7: the carrier of () misses the carrier of () by ;
A8: the InternalRel of () misses the InternalRel of ()
proof
set IG1 = the InternalRel of ();
set IG2 = the InternalRel of ();
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
A9: 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
A10: a = [c1,c2] and
A11: c1 in component x and
c2 in component x 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 () /\ A2 by ;
hence contradiction by A6, A3, A7; :: thesis: verum
end;
A12: the InternalRel of () = the InternalRel of R \ the InternalRel of ()
proof
set IG1 = the InternalRel of ();
set IG2 = the InternalRel of ();
thus the InternalRel of () c= the InternalRel of R \ the InternalRel of () :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of R \ the InternalRel 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 () )
assume A13: a in the InternalRel of () ; :: thesis: a in the InternalRel of R \ the InternalRel of ()
then consider g1, g2 being object such that
A14: a = [g1,g2] and
A15: ( g1 in A2 & g2 in A2 ) by ;
reconsider g1 = g1, g2 = g2 as Element of () by ;
reconsider u1 = g1, u2 = g2 as Element of R by A15;
A16: not a in the InternalRel of () by ;
g1 <= g2 by ;
then u1 <= u2 by YELLOW_0:59;
then a in the InternalRel of R by ;
hence a in the InternalRel of R \ the InternalRel 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 () or a in the InternalRel of () )
assume A17: a in the InternalRel of R \ the InternalRel of () ; :: thesis: a in the InternalRel of ()
then A18: a in the InternalRel of R by XBOOLE_0:def 5;
A19: not a in the InternalRel of () by ;
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 ;
reconsider c1 = c1, c2 = c2 as Element of R by A21;
A22: c1 <= c2 by ;
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 ;
suppose A23: ( c1 in component x & c2 in component x ) ; :: 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 A24: ( c1 in component x & c2 in A2 ) ; :: thesis: a in the InternalRel of ()
A25: [:(),A2:] misses the InternalRel of R
proof
assume not [:(),A2:] misses the InternalRel of R ; :: thesis: contradiction
then [:(),A2:] /\ the InternalRel of R <> {} ;
then consider b being object such that
A26: b in [:(),A2:] /\ the InternalRel of R by XBOOLE_0:def 1;
A27: b in the InternalRel of R by ;
b in [:(),A2:] by ;
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 ;
then [x,b2] in EqCl the InternalRel of R by ;
then b2 in component x by Th29;
then b2 in () /\ A2 by ;
hence contradiction by A6, A3, A7; :: thesis: verum
end;
a in [:(),A2:] by ;
then a in [:(),A2:] /\ the InternalRel of R by ;
hence a in the InternalRel of () by A25; :: thesis: verum
end;
suppose A31: ( c1 in A2 & c2 in component x ) ; :: thesis: a in the InternalRel of ()
A32: [:A2,():] misses the InternalRel of R
proof
assume not [:A2,():] misses the InternalRel of R ; :: thesis: contradiction
then [:A2,():] /\ the InternalRel of R <> {} ;
then consider b being object such that
A33: b in [:A2,():] /\ the InternalRel of R by XBOOLE_0:def 1;
b in [:A2,():] by ;
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 ;
A38: the InternalRel of R c= EqCl the InternalRel of R by MSUALG_5:def 1;
b in the InternalRel of R by ;
then [b2,b1] in EqCl the InternalRel of R by ;
then [x,b1] in EqCl the InternalRel of R by ;
then b1 in component x by Th29;
then b1 in () /\ A2 by ;
hence contradiction by A6, A3, A7; :: thesis: verum
end;
a in [:A2,():] by ;
then a in [:A2,():] /\ the InternalRel of R by ;
hence a in the InternalRel of () by A32; :: thesis: verum
end;
suppose A39: ( c1 in A2 & c2 in A2 ) ; :: 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;
end;
end;
the InternalRel of R = the InternalRel of () \/ the InternalRel of ()
proof
set IG1 = the InternalRel of ();
set IG2 = the InternalRel of ();
thus the InternalRel of R c= the InternalRel of () \/ the InternalRel of () :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of () \/ the InternalRel 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 () )
assume A40: a in the InternalRel of R ; :: thesis: a in the InternalRel of () \/ the InternalRel of ()
assume not a in the InternalRel of () \/ the InternalRel of () ; :: thesis: contradiction
then ( not a in the InternalRel of () & not a in the InternalRel of () ) by XBOOLE_0:def 3;
hence contradiction by A12, A40, 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 () or a in the InternalRel of R )
assume A41: a in the InternalRel of () \/ the InternalRel of () ; :: thesis: a in the InternalRel of R
per cases ( a in the InternalRel of () or a in the InternalRel of () ) by ;
suppose A42: a in the InternalRel of () ; :: 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 ;
reconsider v = v, w = w as Element of () by ;
reconsider u1 = v, u2 = w as Element of R by A44;
v <= w by ;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by ; :: thesis: verum
end;
suppose A45: a in the InternalRel of () ; :: 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 ;
reconsider v = v, w = w as Element of () by ;
reconsider u1 = v, u2 = w as Element of R by A47;
v <= w by ;
then u1 <= u2 by YELLOW_0:59;
hence a in the InternalRel of R by ; :: thesis: verum
end;
end;
end;
then A48: the InternalRel of R = the InternalRel of (union_of ((),())) by NECKLA_2:def 2;
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 ;
the carrier of R = the carrier of (union_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 #) = union_of (G1,G2) ) by A6, A7, A49, A48; :: thesis: verum