let G be _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 aa being Vertex of H st aa = a holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa & x,y 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 aa being Vertex of H st aa = a holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa & x,y 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 aa being Vertex of H st aa = a holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa & x,y are_adjacent )

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

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

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

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

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

set A = H .reachableFrom aa;
let x be Vertex of G; :: thesis: ( x in S implies ex y being Vertex of G st
( y in H .reachableFrom aa & x,y are_adjacent ) )

assume A5: x in S ; :: thesis: ex y being Vertex of G st
( y in H .reachableFrom aa & x,y are_adjacent )

set T = S \ {x};
A6: S \ {x} c= S by XBOOLE_1:36;
then A7: not b in S \ {x} by A1, A2, Def8;
assume A8: for y being Vertex of G holds
( not y in H .reachableFrom aa or not x,y are_adjacent ) ; :: thesis: contradiction
A9: for W being Walk of G st W is_Walk_from a,b & x in W .vertices() holds
ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() )
proof
let W be Walk of G; :: thesis: ( W is_Walk_from a,b & x in W .vertices() implies ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() ) )

assume that
A10: W is_Walk_from a,b and
A11: x in W .vertices() ; :: thesis: ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() )

A12: now :: thesis: not W .find x = 1
assume W .find x = 1 ; :: thesis: contradiction
then W . (W .find x) = W .first() ;
then W . (W .find x) = a by A10;
then not W . (W .find x) in S by A1, A2, Def8;
hence contradiction by A5, A11, GLIB_001:def 19; :: thesis: verum
end;
consider k being odd Element of NAT such that
A13: k <= len W and
A14: W . k = x by ;
W .find (W . k) <= k by ;
then A15: W .find x <= len W by ;
then A16: (W .find x) + (- 2) <= (len W) + 0 by XREAL_1:7;
0 + 1 <= W .find x by ABIAN:12;
then (2 * 0) + 1 < W .find x by ;
then (2 * 1) + 1 <= W .find x by Th4;
then A17: 3 + (- 2) <= (W .find x) + (- 2) by XREAL_1:7;
then A18: (W .find x) - 2 is Element of NAT by INT_1:3;
then reconsider j = (W .find x) - (2 * 1) as odd Nat ;
set P = W .cut (1,j);
A19: (2 * 0) + 1 <= j by A17;
then A20: ((len (W .cut (1,j))) + 1) + (- 1) = (j + 1) + (- 1) by ;
assume A21: for y being Vertex of G holds
( not y in S \ {x} or not y in W .vertices() ) ; :: thesis: contradiction
A22: for n being odd Nat st n <= j holds
( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )
proof
let n be odd Nat; :: thesis: ( n <= j implies ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n ) )
assume A23: n <= j ; :: thesis: ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )
1 <= n by ABIAN:12;
then 1 + (- 1) <= n + (- 1) by XREAL_1:7;
then A24: n - 1 is Element of NAT by INT_1:3;
then reconsider nu1 = n - 1 as Nat ;
n < j + 1 by ;
then n + (- 1) < (j + 1) + (- 1) by XREAL_1:8;
then A25: (W .cut (1,j)) . (nu1 + 1) = W . (1 + nu1) by ;
now :: thesis: not (W .cut (1,j)) . n in S
A26: (W .cut (1,j)) .vertices() c= W .vertices() by ;
A27: n in NAT by ORDINAL1:def 12;
then (W .cut (1,j)) . n in (W .cut (1,j)) .vertices() by ;
then A28: not (W .cut (1,j)) . n in S \ {x} by ;
n < j + 1 by ;
then A29: n + 0 < (j + 1) + 1 by XREAL_1:8;
A30: S \/ {x} = {x} \/ (S \ {x}) by XBOOLE_1:39;
{x} c= S by ;
then A31: S = {x} \/ (S \ {x}) by ;
A32: n <= len W by ;
assume (W .cut (1,j)) . n in S ; :: thesis: contradiction
then (W .cut (1,j)) . n in {x} by ;
then n < W .find (W . n) by ;
hence contradiction by A27, A32, GLIB_001:115; :: thesis: verum
end;
hence ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n ) by A25; :: thesis: verum
end;
then for n being odd Nat st n <= j holds
not (W .cut (1,j)) . n in S ;
then reconsider HP = W .cut (1,j) as Walk of H by ;
W .first() = a by A10;
then (W .cut (1,j)) . ((2 * 0) + 1) = a by ;
then aa in HP .vertices() by ;
then A33: HP .vertices() c= H .reachableFrom aa by GLIB_002:13;
W .find x < (len W) + 1 by ;
then A34: (W .find x) + (- 2) < ((len W) + 1) + (- 2) by XREAL_1:8;
(W .cut (1,j)) . j is Vertex of G by ;
then reconsider Wj = W . j as Vertex of G by A22;
(len W) + (- 1) < (len W) + 0 by XREAL_1:8;
then j < len W by ;
then W . (j + 1) Joins Wj,W . (j + 2),G by ;
then W . (j + 1) Joins Wj,x,G by ;
(W .cut (1,j)) . j in HP .vertices() by ;
then W . j in HP .vertices() by A22;
hence contradiction by A8, A33, A35; :: thesis: verum
end;
A36: now :: thesis: for W being Walk of G st W is_Walk_from a,b holds
ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() )
let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex y being Vertex of G st
( b2 in S \ {x} & b2 in y .vertices() ) )

assume A37: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st
( b2 in S \ {x} & b2 in y .vertices() )

consider y being Vertex of G such that
A38: y in S and
A39: y in W .vertices() by A1, A2, A37, Th70;
per cases ( y = x or y <> x ) ;
suppose y = x ; :: thesis: ex y being Vertex of G st
( b2 in S \ {x} & b2 in y .vertices() )

hence ex y being Vertex of G st
( y in S \ {x} & y in W .vertices() ) by A9, A37, A39; :: thesis: verum
end;
suppose A40: y <> x ; :: thesis: ex y being Vertex of G st
( b2 in S \ {x} & b2 in y .vertices() )

take y = y; :: thesis: ( y in S \ {x} & y in W .vertices() )
not y in {x} by ;
hence y in S \ {x} by ; :: thesis:
thus y in W .vertices() by A39; :: thesis: verum
end;
end;
end;
x in {x} by TARSKI:def 1;
then A41: S \ {x} <> S by ;
not a in S \ {x} by A1, A2, A6, Def8;
then S \ {x} is VertexSeparator of a,b by A1, A2, A7, A36, Th70;
hence contradiction by A3, A41, A6; :: thesis: verum