let R be non empty symmetric irreflexive RelStr ; ( 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
; 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
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)
;
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;
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):]
XBOOLE_0:def 10 (( 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 ;
TARSKI:def 3 ( 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)
;
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):]
A22:
not
a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]
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;
verum
end;
let a be
object ;
TARSKI:def 3 ( 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):]
;
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;
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):]
XBOOLE_0:def 10 (( 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 Rproof
let a be
object ;
TARSKI:def 3 ( 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
;
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):]
;
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;
verum
end;
let a be
object ;
TARSKI:def 3 ( 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):]
;
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 A46:
a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]
;
a in the InternalRel of Rassume A47:
not
a in the
InternalRel of
R
;
contradictionconsider 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;
verum end; suppose A53:
a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]
;
a in the InternalRel of Rassume A54:
not
a in the
InternalRel of
R
;
contradictionconsider 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;
verum 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; verum