let G be finite chordal _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )

assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )

let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )

assume A3: S is minimal ; :: thesis: for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )

let H be removeVertices of G,S; :: thesis: for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )

let a1 be Vertex of H; :: thesis: ( a = a1 implies ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )

assume A4: a = a1 ; :: thesis: ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )

assume A5: for c being Vertex of G holds
( not c in H .reachableFrom a1 or ex x being Vertex of G st
( x in S & not c,x are_adjacent ) ) ; :: thesis: contradiction
per cases ( S is empty or not S is empty ) ;
suppose S is empty ; :: thesis: contradiction
end;
suppose not S is empty ; :: thesis: contradiction
then reconsider S = S as non empty Subset of () ;
set A = H .reachableFrom a1;
deffunc H1( set ) -> Element of omega = card (() /\ S);
set M = { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } ;
A6: now :: thesis: for x being object st x in { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } holds
x is natural
let x be object ; :: thesis: ( x in { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } implies x is natural )
assume x in { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } ; :: thesis: x is natural
then ex y being Vertex of G st
( x = card (() /\ S) & y in H .reachableFrom a1 ) ;
hence x is natural ; :: thesis: verum
end;
A7: H .reachableFrom a1 is finite ;
A8: { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } is finite from a in H .reachableFrom a1 by ;
then card (() /\ S) in { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } ;
then reconsider M = { H1(x) where x is Vertex of G : x in H .reachableFrom a1 } as non empty finite natural-membered set by ;
set Ga = the inducedSubgraph of H,();
A9: the_Vertices_of the inducedSubgraph of H,() = H .reachableFrom a1 by GLIB_000:def 37;
max M in M by XXREAL_2:def 8;
then consider c being Vertex of G such that
A10: max M = card (() /\ S) and
A11: c in H .reachableFrom a1 ;
set gcs = () /\ S;
A12: (H .reachableFrom a1) /\ S = {} by A1, A2, Th74;
set Gs = the inducedSubgraph of G,S;
set tVG = the_Vertices_of G;
A13: (2 * 0) + 1 is odd ;
not a in S by A1, A2, Def8;
then A14: (the_Vertices_of G) \ S is non empty Subset of () by XBOOLE_0:def 5;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider A = H .reachableFrom a1 as non empty Subset of () by XBOOLE_1:1;
now :: thesis: for x being object st x in A holds
x in () \ S
let x be object ; :: thesis: ( x in A implies x in () \ S )
assume A15: x in A ; :: thesis: x in () \ S
not x in S by ;
hence x in () \ S by ; :: thesis: verum
end;
then A c= () \ S ;
then reconsider Ga = the inducedSubgraph of H,() as inducedSubgraph of G,A by ;
consider y being Vertex of G such that
A16: y in S and
A17: not c,y are_adjacent by ;
A18: not y in A by ;
set Ay = A \/ {y};
set Gay = the inducedSubgraph of G,(A \/ {y});
y in {y} by TARSKI:def 1;
then A19: y in A \/ {y} by XBOOLE_0:def 3;
c in A \/ {y} by ;
then reconsider ca = c, ya = y as Vertex of the inducedSubgraph of G,(A \/ {y}) by ;
ex yaa being Vertex of G st
( yaa in A & y,yaa are_adjacent ) by A1, A2, A3, A4, A16, Th81;
then y in G .AdjacentSet () by ;
then the inducedSubgraph of G,(A \/ {y}) is connected by Th56;
then consider Wa being Walk of the inducedSubgraph of G,(A \/ {y}) such that
A20: Wa is_Walk_from ca,ya ;
consider P being Path of the inducedSubgraph of G,(A \/ {y}) such that
A21: P is_Walk_from Wa .first() ,Wa .last() and
A22: P is minlength by Th38;
Wa .first() = ca by A20;
then A23: P .first() = ca by A21;
Wa .last() = ya by A20;
then A24: P .last() = y by A21;
c <> y by ;
then not P is trivial by ;
then A25: len P >= 3 by GLIB_001:125;
A26: now :: thesis: not len P < (2 * 2) + 1
assume len P < (2 * 2) + 1 ; :: thesis: contradiction
then len P <= 5 - 2 by Th3;
then A27: len P = 3 by ;
then (2 * 0) + 1 < len P ;
then P . (1 + 1) Joins P . 1,P . (1 + 2), the inducedSubgraph of G,(A \/ {y}) by GLIB_001:def 3;
then P . 2 Joins c,y,G by ;
hence contradiction by A17; :: thesis: verum
end;
then 5 + (- 2) <= (len P) + (- 2) by XREAL_1:7;
then reconsider j = (len P) - (2 * 1) as odd Element of NAT by ;
set d = P . j;
A28: j < len P by XREAL_1:44;
A29: now :: thesis: not P . j = y
assume P . j = y ; :: thesis: contradiction
then (len P) - 2 = 1 by ;
then len P = 1 + 2 ;
hence contradiction by A26; :: thesis: verum
end;
A30: not y in G .AdjacentSet {c} by ;
A31: the_Vertices_of the inducedSubgraph of G,(A \/ {y}) = A \/ {y} by GLIB_000:def 37;
A32: P . j in the_Vertices_of the inducedSubgraph of G,(A \/ {y}) by ;
then A33: ( P . j in A or P . j in {y} ) by ;
reconsider d = P . j as Vertex of G by A32;
set gds = () /\ S;
P . (j + 1) Joins d,P . (((len P) - 2) + 2), the inducedSubgraph of G,(A \/ {y}) by ;
then A34: P . (j + 1) Joins d,y,G by ;
then d,y are_adjacent ;
then A35: y in G .AdjacentSet {d} by ;
then A36: y in () /\ S by ;
now :: thesis: not () /\ S c= () /\ S
assume A37: (G .AdjacentSet {c}) /\ S c= () /\ S ; :: thesis: contradiction
not y in () /\ S by ;
then (G .AdjacentSet {c}) /\ S c< () /\ S by ;
then A38: card (() /\ S) < card (() /\ S) by TREES_1:6;
card (() /\ S) in M by ;
hence contradiction by A10, A38, XXREAL_2:def 8; :: thesis: verum
end;
then consider x being object such that
A39: x in () /\ S and
A40: not x in () /\ S ;
A41: x in S by ;
then A42: not x in G .AdjacentSet {d} by ;
reconsider x = x as Vertex of G by A39;
defpred S1[ Nat] means ( \$1 in dom P & \$1 is odd & \$1 < len P & ex e being object st e Joins x,P . \$1,G );
A43: for k being Nat st S1[k] holds
k <= len P ;
A44: not x in A by ;
A45: 1 < len P by ;
then A46: 1 in dom P by FINSEQ_3:25;
x in G .AdjacentSet {c} by ;
then c,x are_adjacent by Th51;
then ex e being object st e Joins x,P . 1,G by ;
then A47: ex k being Nat st S1[k] by ;
consider k being Nat such that
A48: S1[k] and
A49: for i being Nat st S1[i] holds
k >= i from reconsider k = k as odd Element of NAT by A48;
set Q1 = P .cut (k,j);
reconsider Q = P .cut (k,j) as Path of G by GLIB_001:175;
A50: k <= j by ;
A51: j < len P by XREAL_1:44;
then A52: P .cut (k,j) is minlength by ;
A53: (len Q) + k = j + 1 by ;
A54: now :: thesis: for i being odd Nat st i in dom Q & i <> 1 holds
for e being object holds not e Joins Q . i,x,G
let i be odd Nat; :: thesis: ( i in dom Q & i <> 1 implies for e being object holds not e Joins Q . i,x,G )
assume that
A55: i in dom Q and
A56: i <> 1 ; :: thesis: for e being object holds not e Joins Q . i,x,G
1 <= i by ;
then 1 + (- 1) <= i + (- 1) by XREAL_1:7;
then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;
reconsider ki1 = k + i1 as odd Element of NAT ;
A57: i + (- 1) < i + () by XREAL_1:8;
i <= len Q by ;
then A58: i1 < len Q by ;
then A59: ki1 in dom P by ;
A60: (len P) + (- 1) < (len P) + () by XREAL_1:8;
assume A61: ex e being object st e Joins Q . i,x,G ; :: thesis: contradiction
i1 + k < (((len P) - 1) - k) + k by ;
then A62: ki1 < len P by ;
A63: Q . (i1 + 1) = P . ki1 by ;
hence contradiction by A56; :: thesis: verum
end;
set cc = Q .first() ;
set dd = Q .last() ;
A64: (P .cut (k,j)) .first() = P . k by ;
then A65: x,Q .first() are_adjacent by A48;
A66: x <> y by ;
then A67: not x in {y} by TARSKI:def 1;
reconsider xs = x, ys = y as Vertex of the inducedSubgraph of G,S by ;
the inducedSubgraph of G,S is complete by A1, A2, A3, Th97;
then xs,ys are_adjacent by A66;
then consider ej being object such that
A68: ej Joins xs,ys, the inducedSubgraph of G,S ;
ej Joins x,y,G by ;
then A69: x,y are_adjacent ;
A70: (P .cut (k,j)) .last() = P . j by ;
then A71: Q .last() = P . j ;
d <> x by ;
then A72: not d,x are_adjacent by ;
then A73: Q .first() <> Q .last() by ;
then A74: Q is open ;
A75: Q .vertices() = (P .cut (k,j)) .vertices() by GLIB_001:98;
then Q .last() in (P .cut (k,j)) .vertices() by GLIB_001:88;
then A76: Q .last() <> x by ;
A77: now :: thesis: not P . k = P . (len P)
A78: (2 * 0) + 1 <= k by ABIAN:12;
then A79: (len (P .cut (1,k))) + 1 = k + 1 by ;
assume P . k = P . (len P) ; :: thesis: contradiction
then P .cut (1,k) is_Walk_from P .first() ,P .last() by ;
hence contradiction by A22, A48, A79; :: thesis: verum
end;
A80: now :: thesis: for v being set st v in Q .vertices() holds
v in A
let v be set ; :: thesis: ( v in Q .vertices() implies v in A )
assume A81: v in Q .vertices() ; :: thesis: v in A
consider n being odd Element of NAT such that
A82: n <= len Q and
A83: Q . n = v by ;
1 <= n by ABIAN:12;
then 1 + (- 1) <= n + (- 1) by XREAL_1:7;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:3;
reconsider kn1 = k + n1 as odd Element of NAT ;
A84: (len P) + (- 1) < (len P) + () by XREAL_1:8;
n + (- 1) < n + () by XREAL_1:8;
then A85: n1 < len Q by ;
then k + n1 < (((len P) - 1) - k) + k by ;
then A86: kn1 < len P by ;
A87: Q . (n1 + 1) = P . kn1 by ;
now :: thesis: not v = y
A88: 1 <= k by ABIAN:12;
assume A89: v = y ; :: thesis: contradiction
then A90: k + (n + (- 1)) = 1 by ;
A91: now :: thesis: not 1 < n
assume 1 < n ; :: thesis: contradiction
then 1 + 1 <= n by NAT_1:13;
then 2 + 1 <= k + n by ;
hence contradiction by A90; :: thesis: verum
end;
1 <= n by ABIAN:12;
hence contradiction by A24, A77, A64, A83, A89, A91, XXREAL_0:1; :: thesis: verum
end;
then A92: not v in {y} by TARSKI:def 1;
Q .vertices() c= P .vertices() by ;
then v in P .vertices() by A81;
hence v in A by ; :: thesis: verum
end;
Q .first() in (P .cut (k,j)) .vertices() by ;
then A93: Q .first() <> x by ;
Q .last() ,y are_adjacent by ;
then consider R being Path of G such that
A94: len R = 7 and
A95: R .length() = 3 and
A96: R .vertices() = {(),y,x,()} and
A97: R . 1 = Q .last() and
A98: R . 3 = y and
A99: R . 5 = x and
A100: R . 7 = Q .first() by A24, A29, A66, A69, A77, A64, A70, A76, A93, A65, Th47;
A101: not R is trivial by ;
A102: Q .edges() misses R .edges()
proof
assume not Q .edges() misses R .edges() ; :: thesis: contradiction
then (Q .edges()) /\ () <> {} ;
then consider e being object such that
A103: e in () /\ () by XBOOLE_0:def 1;
A104: e in Q .edges() by ;
e in R .edges() by ;
then consider n being even Element of NAT such that
A105: 1 <= n and
A106: n <= 7 and
A107: R . n = e by ;
per cases ( n = 2 or n = 4 or n = 6 ) by ;
end;
end;
now :: thesis: for v being object st v in {(),()} holds
v in () /\ ()
let v be object ; :: thesis: ( v in {(),()} implies b1 in () /\ () )
assume A111: v in {(),()} ; :: thesis: b1 in () /\ ()
end;
then A116: {(),()} c= () /\ () ;
now :: thesis: for v being object st v in () /\ () holds
v in {(),()}
let v be object ; :: thesis: ( v in () /\ () implies v in {(),()} )
assume A117: v in () /\ () ; :: thesis: v in {(),()}
v in {(),y,x,()} by ;
then A118: ( v = Q .last() or v = y or v = x or v = Q .first() ) by ENUMSET1:def 2;
v in Q .vertices() by ;
then v in A by A80;
hence v in {(),()} by ; :: thesis: verum
end;
then (Q .vertices()) /\ () c= {(),()} ;
then A119: (Q .vertices()) /\ () = {(),()} by A116;
A120: now :: thesis: for i being odd Nat st i in dom Q & i <> len Q holds
for e being object holds not e Joins Q . i,y,G
let i be odd Nat; :: thesis: ( i in dom Q & i <> len Q implies for e being object holds not e Joins Q . i,y,G )
assume that
A121: i in dom Q and
A122: i <> len Q ; :: thesis: for e being object holds not e Joins Q . i,y,G
1 <= i by ;
then 1 + (- 1) <= i + (- 1) by XREAL_1:7;
then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;
reconsider ki1 = k + i1 as odd Element of NAT ;
A123: i + (- 1) < i + () by XREAL_1:8;
A124: i <= len Q by ;
then A125: i1 < len Q by ;
then ki1 in dom P by ;
then A126: ki1 <= len P by FINSEQ_3:25;
then A127: P . ki1 in A \/ {y} by ;
now :: thesis: not ki1 = len P
A128: ((len P) - k) + (- 1) < (len P) - k by XREAL_1:30;
assume ki1 = len P ; :: thesis: contradiction
hence contradiction by A53, A124, A123, A128, XXREAL_0:2; :: thesis: verum
end;
then ki1 < len P by ;
then A129: ki1 + 2 <= len P by Th4;
ki1 + 2 <> len P by ;
then A130: ki1 + 2 < len P by ;
A131: P . (len P) in A \/ {y} by ;
assume A132: ex e being object st e Joins Q . i,y,G ; :: thesis: contradiction
Q . (i1 + 1) = P . ki1 by ;
hence contradiction by A22, A24, A132, A130, A127, A131, Th19, Th39; :: thesis: verum
end;
A133: Q .first() = P . k by A64;
P . k <> P . j by ;
then A134: not Q is trivial by ;
then Q .length() <> 0 ;
then A135: Q .length() >= 0 + 1 by NAT_1:13;
set C = Q .append R;
A136: R .first() = Q .last() by A97;
then A137: (Q .append R) . ((len Q) + 6) = R . (6 + 1) by ;
A138: (Q .append R) . ((len Q) + 4) = R . (4 + 1) by ;
A139: (Q .append R) . ((len Q) + 2) = R . (2 + 1) by ;
(Q .append R) .length() = () + 3 by ;
then (Q .append R) .length() >= 1 + 3 by ;
then A140: (Q .append R) .length() > 3 by NAT_1:13;
A141: R .last() = Q .first() by ;
then A142: R is open by ;
then Q .append R is Cycle-like by ;
then Q .append R is chordal by ;
then consider m, n being odd Nat such that
A143: m + 2 < n and
A144: n <= len (Q .append R) and
(Q .append R) . m <> (Q .append R) . n and
A145: ex e being object st e Joins (Q .append R) . m,(Q .append R) . n,G and
A146: ( Q .append R is Cycle-like implies ( ( not m = 1 or not n = len (Q .append R) ) & ( not m = 1 or not n = (len (Q .append R)) - 2 ) & ( not m = 3 or not n = len (Q .append R) ) ) ) by Th83;
consider e being object such that
A147: e Joins (Q .append R) . m,(Q .append R) . n,G by A145;
A148: ((len (Q .append R)) + 1) + (- 1) = ((len Q) + (len R)) + (- 1) by ;
A149: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
proof
per cases ( n <= len Q or n > len Q ) ;
suppose n <= len Q ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis: verum
end;
suppose n > len Q ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
then A150: (len Q) + 2 <= n by Th4;
per cases ) + 2 = n or (len Q) + 2 < n ) by ;
suppose (len Q) + 2 = n ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis: verum
end;
suppose (len Q) + 2 < n ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
then A151: ((len Q) + 2) + 2 <= n by Th4;
per cases ) + 4 = n or (len Q) + (2 * 2) < n ) by ;
suppose (len Q) + 4 = n ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis: verum
end;
suppose (len Q) + (2 * 2) < n ; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
then ((len Q) + 4) + 2 <= n by Th4;
hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A152: 1 <= m by ABIAN:12;
per cases ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) by A149;
suppose A158: n = (len Q) + 4 ; :: thesis: contradiction
end;
suppose A161: n = (len Q) + 6 ; :: thesis: contradiction
then (m + 2) + 2 <= (len Q) + 6 by ;
then m + 4 <= ((len Q) + 2) + 4 ;
then A162: m <= (len Q) + 2 by XREAL_1:6;
per cases ( m < (len Q) + 2 or m = (len Q) + 2 ) by ;
end;
end;
end;
end;
end;