let G be non empty symmetric irreflexive RelStr ; :: thesis: for x being Element of G
for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds
G embeds Necklace 4

let x be Element of G; :: thesis: for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds
G embeds Necklace 4

let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & not G is trivial & G is path-connected & ComplRelStr G is path-connected implies G embeds Necklace 4 )
assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr (([#] G) \ {x}) = union_of (R1,R2) and
A3: not G is trivial and
A4: G is path-connected and
A5: ComplRelStr G is path-connected ; :: thesis:
consider a being Element of R1 such that
A6: [a,x] in the InternalRel of G by A1, A2, A4, Th37;
set A = the carrier of G \ {x};
set X = {x};
reconsider A = the carrier of G \ {x} as Subset of G ;
set R = subrelstr A;
reconsider R = subrelstr A as non empty symmetric irreflexive RelStr by ;
( R = subrelstr (([#] G) \ {x}) & R = union_of (R2,R1) ) by ;
then consider b being Element of R2 such that
A7: [b,x] in the InternalRel of G by A1, A4, Th37;
reconsider X1 = { y where y is Element of R1 : [y,x] in the InternalRel of G } , Y1 = { y where y is Element of R1 : not [y,x] in the InternalRel of G } , X2 = { y where y is Element of R2 : [y,x] in the InternalRel of G } , Y2 = { y where y is Element of R2 : not [y,x] in the InternalRel of G } as set ;
reconsider X = {x} as Subset of G ;
set H = subrelstr X;
A8: X1 misses Y1
proof
assume not X1 misses Y1 ; :: thesis: contradiction
then consider a being object such that
A9: ( a in X1 & a in Y1 ) by XBOOLE_0:3;
( ex y1 being Element of R1 st
( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st
( y2 = a & not [y2,x] in the InternalRel of G ) ) by A9;
hence contradiction ; :: thesis: verum
end;
A10: a in X1 by A6;
A11: the carrier of R1 = X1 \/ Y1
proof
thus the carrier of R1 c= X1 \/ Y1 :: according to XBOOLE_0:def 10 :: thesis: X1 \/ Y1 c= the carrier of R1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R1 or a in X1 \/ Y1 )
assume A12: a in the carrier of R1 ; :: thesis: a in X1 \/ Y1
per cases ( [a,x] in the InternalRel of G or not [a,x] in the InternalRel of G ) ;
suppose [a,x] in the InternalRel of G ; :: thesis: a in X1 \/ Y1
then a in X1 by A12;
hence a in X1 \/ Y1 by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not [a,x] in the InternalRel of G ; :: thesis: a in X1 \/ Y1
then a in Y1 by A12;
hence a in X1 \/ Y1 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X1 \/ Y1 or a in the carrier of R1 )
assume A13: a in X1 \/ Y1 ; :: thesis: a in the carrier of R1
per cases ( a in X1 or a in Y1 ) by ;
suppose a in X1 ; :: thesis: a in the carrier of R1
then ex y being Element of R1 st
( a = y & [y,x] in the InternalRel of G ) ;
hence a in the carrier of R1 ; :: thesis: verum
end;
suppose a in Y1 ; :: thesis: a in the carrier of R1
then ex y being Element of R1 st
( a = y & not [y,x] in the InternalRel of G ) ;
hence a in the carrier of R1 ; :: thesis: verum
end;
end;
end;
A14: X2 misses Y2
proof
assume not X2 misses Y2 ; :: thesis: contradiction
then consider a being object such that
A15: ( a in X2 & a in Y2 ) by XBOOLE_0:3;
( ex y1 being Element of R2 st
( y1 = a & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st
( y2 = a & not [y2,x] in the InternalRel of G ) ) by A15;
hence contradiction ; :: thesis: verum
end;
A16: the carrier of () misses the carrier of R
proof
assume not the carrier of () misses the carrier of R ; :: thesis: contradiction
then the carrier of () /\ the carrier of R <> {} ;
then X /\ the carrier of R <> {} by YELLOW_0:def 15;
then X /\ A <> {} by YELLOW_0:def 15;
then consider a being object such that
A17: a in X /\ A by XBOOLE_0:def 1;
( a in X & a in A ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
reconsider H = subrelstr X as non empty symmetric irreflexive RelStr by YELLOW_0:def 15;
A18: b in X2 by A7;
A19: the carrier of G = the carrier of R \/ {x}
proof
thus the carrier of G c= the carrier of R \/ {x} :: according to XBOOLE_0:def 10 :: thesis: the carrier of R \/ {x} c= the carrier of G
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of G or a in the carrier of R \/ {x} )
assume A20: a in the carrier of G ; :: thesis: a in the carrier of R \/ {x}
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R \/ {x} or a in the carrier of G )
assume A21: a in the carrier of R \/ {x} ; :: thesis: a in the carrier of G
per cases ( a in the carrier of R or a in {x} ) by ;
suppose a in the carrier of R ; :: thesis: a in the carrier of G
then a in the carrier of G \ {x} by YELLOW_0:def 15;
hence a in the carrier of G ; :: thesis: verum
end;
suppose a in {x} ; :: thesis: a in the carrier of G
hence a in the carrier of G ; :: thesis: verum
end;
end;
end;
A22: the carrier of R2 = X2 \/ Y2
proof
thus the carrier of R2 c= X2 \/ Y2 :: according to XBOOLE_0:def 10 :: thesis: X2 \/ Y2 c= the carrier of R2
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of R2 or a in X2 \/ Y2 )
assume A23: a in the carrier of R2 ; :: thesis: a in X2 \/ Y2
per cases ( [a,x] in the InternalRel of G or not [a,x] in the InternalRel of G ) ;
suppose [a,x] in the InternalRel of G ; :: thesis: a in X2 \/ Y2
then a in X2 by A23;
hence a in X2 \/ Y2 by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not [a,x] in the InternalRel of G ; :: thesis: a in X2 \/ Y2
then a in Y2 by A23;
hence a in X2 \/ Y2 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X2 \/ Y2 or a in the carrier of R2 )
assume A24: a in X2 \/ Y2 ; :: thesis: a in the carrier of R2
per cases ( a in X2 or a in Y2 ) by ;
suppose a in X2 ; :: thesis: a in the carrier of R2
then ex y being Element of R2 st
( a = y & [y,x] in the InternalRel of G ) ;
hence a in the carrier of R2 ; :: thesis: verum
end;
suppose a in Y2 ; :: thesis: a in the carrier of R2
then ex y being Element of R2 st
( a = y & not [y,x] in the InternalRel of G ) ;
hence a in the carrier of R2 ; :: thesis: verum
end;
end;
end;
A25: not Y1 \/ Y2 is empty
proof
assume A26: Y1 \/ Y2 is empty ; :: thesis: contradiction
then A27: Y2 is empty ;
A28: Y1 is empty by A26;
A29: for a being Element of R holds [a,x] in the InternalRel of G
proof
let a be Element of R; :: thesis: [a,x] in the InternalRel of G
A30: the carrier of R = the carrier of R1 \/ the carrier of R2 by ;
per cases ( a in the carrier of R1 or a in the carrier of R2 ) by ;
suppose a in the carrier of R1 ; :: thesis: [a,x] in the InternalRel of G
then ex y being Element of R1 st
( a = y & [y,x] in the InternalRel of G ) by ;
hence [a,x] in the InternalRel of G ; :: thesis: verum
end;
suppose a in the carrier of R2 ; :: thesis: [a,x] in the InternalRel of G
then ex y being Element of R2 st
( a = y & [y,x] in the InternalRel of G ) by ;
hence [a,x] in the InternalRel of G ; :: thesis: verum
end;
end;
end;
not ComplRelStr G is path-connected
proof
A31: a <> x
proof
assume not a <> x ; :: thesis: contradiction
then x in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A32: x in the carrier of R by ;
x in {x} by TARSKI:def 1;
then x in the carrier of H by YELLOW_0:def 15;
then x in the carrier of R /\ the carrier of H by ;
hence contradiction by A16; :: thesis: verum
end;
a in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A33: a in the carrier of R by ;
the carrier of R c= the carrier of G by ;
then A34: a is Element of () by ;
A35: x is Element of () by NECKLACE:def 8;
assume ComplRelStr G is path-connected ; :: thesis: contradiction
then the InternalRel of () reduces x,a by ;
then consider p being FinSequence such that
A36: len p > 0 and
A37: p . 1 = x and
A38: p . (len p) = a and
A39: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of () by REWRITE1:11;
A40: 0 + 1 <= len p by ;
then len p > 1 by ;
then 1 + 1 <= len p by NAT_1:13;
then A41: 2 in dom p by FINSEQ_3:25;
1 in dom p by ;
then A42: [(p . 1),(p . (1 + 1))] in the InternalRel of () by ;
A43: p . 2 <> x
proof
A44: [x,x] in id the carrier of G by RELAT_1:def 10;
assume not p . 2 <> x ; :: thesis: contradiction
then [x,x] in the InternalRel of () /\ (id the carrier of G) by ;
then the InternalRel of () meets id the carrier of G ;
hence contradiction by Th13; :: thesis: verum
end;
p . 2 in the carrier of () by ;
then A45: p . 2 in the carrier of G by NECKLACE:def 8;
p . 2 in the carrier of R
proof
assume not p . 2 in the carrier of R ; :: thesis: contradiction
then p . 2 in {x} by ;
hence contradiction by A43, TARSKI:def 1; :: thesis: verum
end;
then A46: [(p . 2),x] in the InternalRel of G by A29;
A47: the InternalRel of () is_symmetric_in the carrier of () by NECKLACE:def 3;
( p . 1 in the carrier of () & p . (1 + 1) in the carrier of () ) by ;
then [(p . (1 + 1)),(p . 1)] in the InternalRel of () by ;
then [(p . 2),x] in the InternalRel of () /\ the InternalRel of G by ;
then the InternalRel of () meets the InternalRel of G ;
hence contradiction by Th12; :: thesis: verum
end;
hence contradiction by A5; :: thesis: verum
end;
thus G embeds Necklace 4 :: thesis: verum
proof
per cases ( not Y1 is empty or not Y2 is empty ) by A25;
suppose A48: not Y1 is empty ; :: thesis:
ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G
proof
set b = the Element of Y1;
a in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A49: a in the carrier of R by ;
the Element of Y1 in Y1 by A48;
then ex y being Element of R1 st
( y = the Element of Y1 & not [y,x] in the InternalRel of G ) ;
then the Element of Y1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A50: the Element of Y1 in the carrier of R by ;
A51: the carrier of R c= the carrier of G by ;
then reconsider a = a as Element of G by A49;
reconsider b = the Element of Y1 as Element of G by ;
a <> b
proof
assume A52: not a <> b ; :: thesis: contradiction
a in X1 by A6;
then a in X1 /\ Y1 by ;
hence contradiction by A8; :: thesis: verum
end;
then the InternalRel of G reduces a,b by A4;
then consider p being FinSequence such that
A53: len p > 0 and
A54: p . 1 = a and
A55: p . (len p) = b and
A56: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of G by REWRITE1:11;
defpred S1[ Nat] means ( p . \$1 in Y1 & \$1 in dom p & ( for k being Nat st k > \$1 & k in dom p holds
p . k in Y1 ) );
for k being Nat st k > len p & k in dom p holds
p . k in Y1
proof
let k be Nat; :: thesis: ( k > len p & k in dom p implies p . k in Y1 )
assume A57: k > len p ; :: thesis: ( not k in dom p or p . k in Y1 )
assume k in dom p ; :: thesis: p . k in Y1
then k in Seg (len p) by FINSEQ_1:def 3;
hence p . k in Y1 by ; :: thesis: verum
end;
then S1[ len p] by ;
then A58: ex k being Nat st S1[k] ;
ex n0 being Nat st
( S1[n0] & ( for n being Nat st S1[n] holds
n >= n0 ) ) from then consider n0 being Nat such that
A59: S1[n0] and
A60: for n being Nat st S1[n] holds
n >= n0 ;
n0 <> 0
proof
assume not n0 <> 0 ; :: thesis: contradiction
then 0 in Seg (len p) by ;
hence contradiction by FINSEQ_1:1; :: thesis: verum
end;
then consider k0 being Nat such that
A61: n0 = k0 + 1 by NAT_1:6;
A62: n0 <> 1
proof
assume A63: not n0 <> 1 ; :: thesis: contradiction
a in X1 by A6;
then not X1 /\ Y1 is empty by ;
hence contradiction by A8; :: thesis: verum
end;
A64: k0 >= 1 n0 in Seg (len p) by ;
then ( k0 <= k0 + 1 & n0 <= len p ) by ;
then A65: k0 <= len p by ;
then A66: k0 in dom p by ;
then A67: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by ;
then A68: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by ;
p . n0 in the carrier of G by ;
then A69: [(p . n0),(p . k0)] in the InternalRel of G by ;
A70: for k being Nat st k > k0 & k in dom p holds
p . k in Y1
proof
assume ex k being Nat st
( k > k0 & k in dom p & not p . k in Y1 ) ; :: thesis: contradiction
then consider k being Nat such that
A71: k > k0 and
A72: k in dom p and
A73: not p . k in Y1 ;
k > n0
proof
per cases ( k < n0 or n0 < k or n0 = k ) by XXREAL_0:1;
suppose k < n0 ; :: thesis: k > n0
hence k > n0 by ; :: thesis: verum
end;
suppose n0 < k ; :: thesis: k > n0
hence k > n0 ; :: thesis: verum
end;
suppose n0 = k ; :: thesis: k > n0
hence k > n0 by ; :: thesis: verum
end;
end;
end;
hence contradiction by A59, A72, A73; :: thesis: verum
end;
k0 < n0 by ;
then A74: not S1[k0] by A60;
p . k0 in the carrier of G by ;
then ( p . k0 in the carrier of R or p . k0 in {x} ) by ;
then A75: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by ;
thus ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G :: thesis: verum
proof
per cases ( ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) or ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) or ( p . k0 in {x} & p . n0 in the carrier of G ) ) by ;
suppose A76: ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) ; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G
then reconsider m = p . k0 as Element of X1 by ;
m in the carrier of R1 \/ the carrier of R2 by ;
then A77: m in the carrier of R by ;
reconsider l = p . n0 as Element of Y1 by A59;
A78: the carrier of R c= the carrier of G by ;
l in the carrier of R1 by ;
then l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A79: l in the carrier of R by ;
( [m,l] in the InternalRel of G & the InternalRel of G is_symmetric_in the carrier of G ) by ;
then [l,m] in the InternalRel of G by ;
hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G ; :: thesis: verum
end;
suppose ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) ; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G
then reconsider m = p . k0 as Element of R2 ;
reconsider l = p . n0 as Element of R1 by ;
m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A80: m in the carrier of R by ;
l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then l in the carrier of R by ;
then [l,m] in [: the carrier of R, the carrier of R:] by ;
then [l,m] in the InternalRel of G |_2 the carrier of R by ;
then [l,m] in the InternalRel of R by YELLOW_0:def 14;
hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by A1, A2, Th35; :: thesis: verum
end;
suppose A81: ( p . k0 in {x} & p . n0 in the carrier of G ) ; :: thesis: ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G
ex y1 being Element of R1 st
( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A59;
hence ex b being Element of Y1 ex c being Element of X1 st [b,c] in the InternalRel of G by ; :: thesis: verum
end;
end;
end;
end;
then consider u being Element of Y1, v being Element of X1 such that
A82: [u,v] in the InternalRel of G ;
set w = the Element of X2;
the Element of X2 in X2 by A18;
then A83: ex y being Element of R2 st
( y = the Element of X2 & [y,x] in the InternalRel of G ) ;
set Z = {u,v,x, the Element of X2};
{u,v,x, the Element of X2} c= the carrier of G
proof
the Element of X2 in X2 by A18;
then ex y2 being Element of R2 st
( y2 = the Element of X2 & [y2,x] in the InternalRel of G ) ;
then the Element of X2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A84: the Element of X2 in the carrier of R by ;
v in X1 by A10;
then ex y1 being Element of R1 st
( y1 = v & [y1,x] in the InternalRel of G ) ;
then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A85: v in the carrier of R by ;
u in the carrier of R1 by ;
then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A86: u in the carrier of R by ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X2} or q in the carrier of G )
assume q in {u,v,x, the Element of X2} ; :: thesis: q in the carrier of G
then A87: ( q = u or q = v or q = x or q = the Element of X2 ) by ENUMSET1:def 2;
the carrier of R c= the carrier of G by ;
hence q in the carrier of G by A87, A86, A85, A84; :: thesis: verum
end;
then reconsider Z = {u,v,x, the Element of X2} as Subset of G ;
reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;
A88: the Element of X2 in X2 by A18;
reconsider w = the Element of X2 as Element of G by ;
A89: v in X1 by A10;
A90: [x,w] in the InternalRel of G
proof
( ex y1 being Element of R2 st
( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by ;
hence [x,w] in the InternalRel of G ; :: thesis: verum
end;
A91: u in Y1 by A48;
reconsider u = u, v = v as Element of G by ;
A92: [v,x] in the InternalRel of G
proof
ex y1 being Element of R1 st
( v = y1 & [y1,x] in the InternalRel of G ) by A89;
hence [v,x] in the InternalRel of G ; :: thesis: verum
end;
A93: w <> u
proof
assume A94: not w <> u ; :: thesis: contradiction
( ex y1 being Element of R2 st
( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st
( u = y2 & not [y2,x] in the InternalRel of G ) ) by ;
hence contradiction by A94; :: thesis: verum
end;
A95: not [u,x] in the InternalRel of G
proof
ex y1 being Element of R1 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A91;
hence not [u,x] in the InternalRel of G ; :: thesis: verum
end;
A96: not [v,w] in the InternalRel of G
proof
A97: ex y2 being Element of R2 st
( w = y2 & [y2,x] in the InternalRel of G ) by A88;
then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w = w as Element of R by ;
A98: ex y1 being Element of R1 st
( v = y1 & [y1,x] in the InternalRel of G ) by A89;
then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider v = v as Element of R by ;
assume [v,w] in the InternalRel of G ; :: thesis: contradiction
then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;
then [v,w] in the InternalRel of R by YELLOW_0:def 14;
then A99: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by ;
per cases ( [v,w] in the InternalRel of R1 or [v,w] in the InternalRel of R2 ) by ;
suppose [v,w] in the InternalRel of R1 ; :: thesis: contradiction
then w in the carrier of R1 by ZFMISC_1:87;
then w in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
suppose [v,w] in the InternalRel of R2 ; :: thesis: contradiction
then v in the carrier of R2 by ZFMISC_1:87;
then v in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
A100: w <> x
proof
assume A101: not w <> x ; :: thesis: contradiction
ex y1 being Element of R2 st
( w = y1 & [y1,x] in the InternalRel of G ) by A88;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A102: not [u,w] in the InternalRel of G
proof
A103: ex y2 being Element of R2 st
( w = y2 & [y2,x] in the InternalRel of G ) by A88;
then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w = w as Element of R by ;
A104: ex y1 being Element of R1 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A91;
then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider u = u as Element of R by ;
assume [u,w] in the InternalRel of G ; :: thesis: contradiction
then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;
then [u,w] in the InternalRel of R by YELLOW_0:def 14;
then A105: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by ;
per cases ( [u,w] in the InternalRel of R1 or [u,w] in the InternalRel of R2 ) by ;
suppose [u,w] in the InternalRel of R1 ; :: thesis: contradiction
then w in the carrier of R1 by ZFMISC_1:87;
then w in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
suppose [u,w] in the InternalRel of R2 ; :: thesis: contradiction
then u in the carrier of R2 by ZFMISC_1:87;
then u in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
A106: x <> u
proof
assume A107: not x <> u ; :: thesis: contradiction
ex y1 being Element of R1 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A91;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A108: w <> v
proof
consider y1 being Element of R2 such that
A109: w = y1 and
[y1,x] in the InternalRel of G by A88;
assume A110: not w <> v ; :: thesis: contradiction
ex y2 being Element of R1 st
( v = y2 & [y2,x] in the InternalRel of G ) by A89;
then y1 in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
A111: v <> x
proof
assume A112: not v <> x ; :: thesis: contradiction
ex y1 being Element of R1 st
( v = y1 & [y1,x] in the InternalRel of G ) by A89;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
u <> v
proof
assume A113: not u <> v ; :: thesis: contradiction
( ex y1 being Element of R1 st
( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R1 st
( v = y2 & [y2,x] in the InternalRel of G ) ) by ;
hence contradiction by A113; :: thesis: verum
end;
then u,v,x,w are_mutually_distinct by ;
then A114: subrelstr Z embeds Necklace 4 by A82, A92, A90, A95, A102, A96, Th38;
G embeds Necklace 4 hence G embeds Necklace 4 ; :: thesis: verum
end;
suppose A115: not Y2 is empty ; :: thesis:
ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G
proof
set c = the Element of Y2;
b in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A116: b in the carrier of R by ;
the Element of Y2 in Y2 by A115;
then ex y being Element of R2 st
( y = the Element of Y2 & not [y,x] in the InternalRel of G ) ;
then the Element of Y2 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A117: the Element of Y2 in the carrier of R by ;
A118: the carrier of R c= the carrier of G by ;
then reconsider b = b as Element of G by A116;
reconsider c = the Element of Y2 as Element of G by ;
b <> c
proof
assume not b <> c ; :: thesis: contradiction
then c in X2 by A7;
then c in X2 /\ Y2 by ;
hence contradiction by A14; :: thesis: verum
end;
then the InternalRel of G reduces b,c by A4;
then consider p being FinSequence such that
A119: len p > 0 and
A120: p . 1 = b and
A121: p . (len p) = c and
A122: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of G by REWRITE1:11;
defpred S1[ Nat] means ( p . \$1 in Y2 & \$1 in dom p & ( for k being Nat st k > \$1 & k in dom p holds
p . k in Y2 ) );
for k being Nat st k > len p & k in dom p holds
p . k in Y2
proof
let k be Nat; :: thesis: ( k > len p & k in dom p implies p . k in Y2 )
assume A123: k > len p ; :: thesis: ( not k in dom p or p . k in Y2 )
assume k in dom p ; :: thesis: p . k in Y2
then k in Seg (len p) by FINSEQ_1:def 3;
hence p . k in Y2 by ; :: thesis: verum
end;
then S1[ len p] by ;
then A124: ex k being Nat st S1[k] ;
ex n0 being Nat st
( S1[n0] & ( for n being Nat st S1[n] holds
n >= n0 ) ) from then consider n0 being Nat such that
A125: S1[n0] and
A126: for n being Nat st S1[n] holds
n >= n0 ;
n0 <> 0
proof
assume not n0 <> 0 ; :: thesis: contradiction
then 0 in Seg (len p) by ;
hence contradiction by FINSEQ_1:1; :: thesis: verum
end;
then consider k0 being Nat such that
A127: n0 = k0 + 1 by NAT_1:6;
A128: n0 <> 1
proof
assume A129: not n0 <> 1 ; :: thesis: contradiction
b in X2 by A7;
then not X2 /\ Y2 is empty by ;
hence contradiction by A14; :: thesis: verum
end;
A130: k0 >= 1 n0 in Seg (len p) by ;
then ( k0 <= k0 + 1 & n0 <= len p ) by ;
then k0 <= len p by ;
then A131: k0 in Seg (len p) by ;
then A132: k0 in dom p by FINSEQ_1:def 3;
then A133: [(p . k0),(p . (k0 + 1))] in the InternalRel of G by ;
then A134: ( the InternalRel of G is_symmetric_in the carrier of G & p . k0 in the carrier of G ) by ;
p . n0 in the carrier of G by ;
then A135: [(p . n0),(p . k0)] in the InternalRel of G by ;
A136: for k being Nat st k > k0 & k in dom p holds
p . k in Y2
proof
assume ex k being Nat st
( k > k0 & k in dom p & not p . k in Y2 ) ; :: thesis: contradiction
then consider k being Nat such that
A137: k > k0 and
A138: k in dom p and
A139: not p . k in Y2 ;
k > n0
proof
per cases ( k < n0 or n0 < k or n0 = k ) by XXREAL_0:1;
suppose k < n0 ; :: thesis: k > n0
hence k > n0 by ; :: thesis: verum
end;
suppose n0 < k ; :: thesis: k > n0
hence k > n0 ; :: thesis: verum
end;
suppose n0 = k ; :: thesis: k > n0
hence k > n0 by ; :: thesis: verum
end;
end;
end;
hence contradiction by A125, A138, A139; :: thesis: verum
end;
k0 < n0 by ;
then A140: not S1[k0] by A126;
p . k0 in the carrier of G by ;
then ( p . k0 in the carrier of R or p . k0 in {x} ) by ;
then A141: ( p . k0 in the carrier of R1 \/ the carrier of R2 or p . k0 in {x} ) by ;
thus ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G :: thesis: verum
proof
per cases ( ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) or ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) or ( p . k0 in {x} & p . n0 in the carrier of G ) ) by ;
suppose ( p . k0 in the carrier of R2 & p . n0 in the carrier of G ) ; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G
then reconsider m = p . k0 as Element of X2 by ;
reconsider l = p . n0 as Element of Y2 by A125;
[m,l] in the InternalRel of G by ;
hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A135; :: thesis: verum
end;
suppose ( p . k0 in the carrier of R1 & p . n0 in the carrier of G ) ; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G
then reconsider m = p . k0 as Element of R1 ;
reconsider l = p . n0 as Element of R2 by ;
A142: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
m in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A143: m in the carrier of R by ;
l in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A144: l in the carrier of R by ;
then [l,m] in [: the carrier of R, the carrier of R:] by ;
then [l,m] in the InternalRel of G |_2 the carrier of R by ;
then [l,m] in the InternalRel of R by YELLOW_0:def 14;
then [m,l] in the InternalRel of R by ;
hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by A1, A2, Th35; :: thesis: verum
end;
suppose A145: ( p . k0 in {x} & p . n0 in the carrier of G ) ; :: thesis: ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G
ex y1 being Element of R2 st
( p . n0 = y1 & not [y1,x] in the InternalRel of G ) by A125;
hence ex c being Element of Y2 ex d being Element of X2 st [c,d] in the InternalRel of G by ; :: thesis: verum
end;
end;
end;
end;
then consider u being Element of Y2, v being Element of X2 such that
A146: [u,v] in the InternalRel of G ;
set w = the Element of X1;
the Element of X1 in X1 by A10;
then A147: ex y being Element of R1 st
( y = the Element of X1 & [y,x] in the InternalRel of G ) ;
set Z = {u,v,x, the Element of X1};
{u,v,x, the Element of X1} c= the carrier of G
proof
the Element of X1 in X1 by A10;
then ex y2 being Element of R1 st
( y2 = the Element of X1 & [y2,x] in the InternalRel of G ) ;
then the Element of X1 in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A148: the Element of X1 in the carrier of R by ;
v in X2 by A18;
then ex y1 being Element of R2 st
( y1 = v & [y1,x] in the InternalRel of G ) ;
then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A149: v in the carrier of R by ;
u in the carrier of R2 by ;
then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then A150: u in the carrier of R by ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {u,v,x, the Element of X1} or q in the carrier of G )
assume q in {u,v,x, the Element of X1} ; :: thesis: q in the carrier of G
then A151: ( q = u or q = v or q = x or q = the Element of X1 ) by ENUMSET1:def 2;
the carrier of R c= the carrier of G by ;
hence q in the carrier of G by ; :: thesis: verum
end;
then reconsider Z = {u,v,x, the Element of X1} as Subset of G ;
reconsider H = subrelstr Z as non empty full SubRelStr of G by YELLOW_0:def 15;
A152: the Element of X1 in X1 by A10;
reconsider w = the Element of X1 as Element of G by ;
A153: v in X2 by A18;
A154: [x,w] in the InternalRel of G
proof
( ex y1 being Element of R1 st
( w = y1 & [y1,x] in the InternalRel of G ) & the InternalRel of G is_symmetric_in the carrier of G ) by ;
hence [x,w] in the InternalRel of G ; :: thesis: verum
end;
A155: u in Y2 by A115;
reconsider u = u, v = v as Element of G by ;
A156: [v,x] in the InternalRel of G
proof
ex y1 being Element of R2 st
( v = y1 & [y1,x] in the InternalRel of G ) by A153;
hence [v,x] in the InternalRel of G ; :: thesis: verum
end;
A157: w <> u
proof
assume A158: not w <> u ; :: thesis: contradiction
( ex y1 being Element of R1 st
( w = y1 & [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st
( u = y2 & not [y2,x] in the InternalRel of G ) ) by ;
hence contradiction by A158; :: thesis: verum
end;
A159: not [u,x] in the InternalRel of G
proof
ex y1 being Element of R2 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A155;
hence not [u,x] in the InternalRel of G ; :: thesis: verum
end;
A160: not [v,w] in the InternalRel of G
proof
A161: ex y2 being Element of R1 st
( w = y2 & [y2,x] in the InternalRel of G ) by A152;
then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w = w as Element of R by ;
A162: ex y1 being Element of R2 st
( v = y1 & [y1,x] in the InternalRel of G ) by A153;
then v in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider v = v as Element of R by ;
assume [v,w] in the InternalRel of G ; :: thesis: contradiction
then [v,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;
then [v,w] in the InternalRel of R by YELLOW_0:def 14;
then A163: [v,w] in the InternalRel of R1 \/ the InternalRel of R2 by ;
per cases ( [v,w] in the InternalRel of R1 or [v,w] in the InternalRel of R2 ) by ;
suppose [v,w] in the InternalRel of R1 ; :: thesis: contradiction
then v in the carrier of R1 by ZFMISC_1:87;
then v in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
suppose [v,w] in the InternalRel of R2 ; :: thesis: contradiction
then w in the carrier of R2 by ZFMISC_1:87;
then w in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
A164: w <> x
proof
assume A165: not w <> x ; :: thesis: contradiction
ex y1 being Element of R1 st
( w = y1 & [y1,x] in the InternalRel of G ) by A152;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A166: not [u,w] in the InternalRel of G
proof
A167: ex y2 being Element of R1 st
( w = y2 & [y2,x] in the InternalRel of G ) by A152;
then w in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w = w as Element of R by ;
A168: ex y1 being Element of R2 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A155;
then u in the carrier of R1 \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider u = u as Element of R by ;
assume [u,w] in the InternalRel of G ; :: thesis: contradiction
then [u,w] in the InternalRel of G |_2 the carrier of R by XBOOLE_0:def 4;
then [u,w] in the InternalRel of R by YELLOW_0:def 14;
then A169: [u,w] in the InternalRel of R1 \/ the InternalRel of R2 by ;
per cases ( [u,w] in the InternalRel of R1 or [u,w] in the InternalRel of R2 ) by ;
suppose [u,w] in the InternalRel of R1 ; :: thesis: contradiction
then u in the carrier of R1 by ZFMISC_1:87;
then u in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
suppose [u,w] in the InternalRel of R2 ; :: thesis: contradiction
then w in the carrier of R2 by ZFMISC_1:87;
then w in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
A170: x <> u
proof
assume A171: not x <> u ; :: thesis: contradiction
ex y1 being Element of R2 st
( u = y1 & not [y1,x] in the InternalRel of G ) by A155;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A172: w <> v
proof
consider y1 being Element of R1 such that
A173: w = y1 and
[y1,x] in the InternalRel of G by A152;
assume A174: not w <> v ; :: thesis: contradiction
ex y2 being Element of R2 st
( v = y2 & [y2,x] in the InternalRel of G ) by A153;
then y1 in the carrier of R1 /\ the carrier of R2 by ;
hence contradiction by A1; :: thesis: verum
end;
A175: v <> x
proof
assume A176: not v <> x ; :: thesis: contradiction
ex y1 being Element of R2 st
( v = y1 & [y1,x] in the InternalRel of G ) by A153;
then x in the carrier of R1 \/ the carrier of R2 by ;
then x in the carrier of R by ;
then x in the carrier of G \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
u <> v
proof
assume A177: not u <> v ; :: thesis: contradiction
( ex y1 being Element of R2 st
( u = y1 & not [y1,x] in the InternalRel of G ) & ex y2 being Element of R2 st
( v = y2 & [y2,x] in the InternalRel of G ) ) by ;
hence contradiction by A177; :: thesis: verum
end;
then u,v,x,w are_mutually_distinct by ;
then A178: subrelstr Z embeds Necklace 4 by ;
G embeds Necklace 4 hence G embeds Necklace 4 ; :: thesis: verum
end;
end;
end;