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

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)

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; :: thesis: verum

( 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 ; :: 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 #) = 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

proof

A9:
the carrier of (subrelstr A2) = A2
by YELLOW_0:def 15;
thus
the carrier of R c= A1 \/ A2
:: according to XBOOLE_0:def 10 :: thesis: A1 \/ A2 c= the carrier of R

assume A8: a in A1 \/ A2 ; :: thesis: a in the carrier of R

end;proof

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

assume A7: a in the carrier of R ; :: thesis: a in A1 \/ A2

assume not a in A1 \/ A2 ; :: thesis: contradiction

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

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

end;assume A7: a in the carrier of R ; :: thesis: a in A1 \/ A2

assume not a in A1 \/ A2 ; :: thesis: contradiction

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

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

assume A8: a in A1 \/ A2 ; :: thesis: a in the carrier of R

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

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):]
assume
not the InternalRel of (subrelstr A1) misses the InternalRel of (subrelstr A2)
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

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):]
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: (( 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)

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):] ; :: thesis: 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;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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) )
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 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) ; :: thesis: 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):]

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; :: thesis: verum

end;assume A16: a in the InternalRel of (subrelstr A2) ; :: thesis: 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):]

proof

A22:
not a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]
assume
a in [: the carrier of (subrelstr A2), the carrier of (subrelstr A1):]
; :: thesis: contradiction

then g2 in A1 by A5, A17, ZFMISC_1:87;

then g2 in A1 /\ A2 by A19, XBOOLE_0:def 4;

hence contradiction by A5, A9, A10; :: thesis: verum

end;then g2 in A1 by A5, A17, ZFMISC_1:87;

then g2 in A1 /\ A2 by A19, XBOOLE_0:def 4;

hence contradiction by A5, A9, A10; :: thesis: verum

proof

g1 <= g2
by A16, A17, ORDERS_2:def 5;
assume
a in [: the carrier of (subrelstr A1), the carrier of (subrelstr A2):]
; :: thesis: contradiction

then g1 in A1 by A5, A17, ZFMISC_1:87;

then g1 in A1 /\ A2 by A18, XBOOLE_0:def 4;

hence contradiction by A5, A9, A10; :: thesis: verum

end;then g1 in A1 by A5, A17, ZFMISC_1:87;

then g1 in A1 /\ A2 by A18, XBOOLE_0:def 4;

hence contradiction by A5, A9, A10; :: thesis: verum

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; :: thesis: verum

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):] ; :: thesis: 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;

per cases
( ( c1 in A1 & c2 in A1 ) or ( c1 in A1 & c2 in A2 ) or ( c1 in A2 & c2 in A1 ) or ( c1 in A2 & c2 in A2 ) )
by A6, XBOOLE_0:def 3;

end;

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

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

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

d1 <= d2 by A5, A31, YELLOW_0:60;

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

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

d1 <= d2 by A5, A31, YELLOW_0:60;

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

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

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

d1 <= d2 by A9, A31, A33, YELLOW_0:60;

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

end;d1 <= d2 by A9, A31, A33, YELLOW_0:60;

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

proof

then A60:
the InternalRel of R = the InternalRel of (sum_of ((subrelstr A1),(subrelstr A2)))
by NECKLA_2:def 3;
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: (( 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 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):] ; :: thesis: 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;

end;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: (( 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 R

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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):] ; :: thesis: 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; :: thesis: verum

end;assume A34: a in the InternalRel of R ; :: thesis: 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):] ; :: thesis: 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; :: thesis: verum

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):] ; :: thesis: 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;

end;

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

then consider v, w being object such that

A41: a = [v,w] and

A42: ( v in A1 & w in A1 ) by A5, RELSET_1:2;

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

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

v <= w by A40, A41, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

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

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

A42: ( v in A1 & w in A1 ) by A5, RELSET_1:2;

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

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

v <= w by A40, A41, ORDERS_2:def 5;

then u1 <= u2 by YELLOW_0:59;

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

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

then consider v, w being object such that

A44: a = [v,w] and

A45: ( v in A2 & w in A2 ) by A9, RELSET_1:2;

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

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

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

then u1 <= u2 by YELLOW_0:59;

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

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

A45: ( v in A2 & w in A2 ) by A9, RELSET_1:2;

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

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

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

then u1 <= u2 by YELLOW_0:59;

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

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

assume A47:
not a in the InternalRel of R
; :: thesis: contradiction

consider 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; :: thesis: verum

end;consider 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; :: thesis: verum

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

assume A54:
not a in the InternalRel of R
; :: thesis: contradiction

consider 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; :: thesis: verum

end;consider 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; :: thesis: verum

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; :: thesis: verum