let R be non empty symmetric irreflexive RelStr ; ( 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
; 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
then A5:
the carrier of R = (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)
proof
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)
;
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;
verum
end;
A12:
the InternalRel of (subrelstr A2) = the InternalRel of R \ the InternalRel of (subrelstr (component x))
proof
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))
XBOOLE_0:def 10 the InternalRel of R \ the InternalRel of (subrelstr (component x)) c= the InternalRel of (subrelstr A2)proof
let a be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) or a in the InternalRel of (subrelstr A2) )
assume A17:
a in the
InternalRel of
R \ the
InternalRel of
(subrelstr (component x))
;
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;
suppose A24:
(
c1 in component x &
c2 in A2 )
;
a in the InternalRel of (subrelstr A2)A25:
[:(component x),A2:] misses the
InternalRel of
R
proof
assume
not
[:(component x),A2:] misses the
InternalRel of
R
;
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;
verum
end;
a in [:(component x),A2:]
by A20, A24, ZFMISC_1:def 2;
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;
verum end; suppose A31:
(
c1 in A2 &
c2 in component x )
;
a in the InternalRel of (subrelstr A2)A32:
[:A2,(component x):] misses the
InternalRel of
R
proof
assume
not
[:A2,(component x):] misses the
InternalRel of
R
;
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;
verum
end;
a in [:A2,(component x):]
by A20, A31, ZFMISC_1:def 2;
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;
verum end;
end;
the InternalRel of R = the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2)
then A48:
the InternalRel of R = the InternalRel of (union_of ((subrelstr (component x)),(subrelstr A2)))
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 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; verum