let G be _Graph; :: thesis:
let a, b be Vertex of G; :: thesis:
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis:
let S be VertexSeparator of a,b; :: thesis:
assume A3: S is minimal ; :: thesis:
let H be removeVertices of G,S; :: thesis:
let aa be Vertex of H; :: thesis:
assume A4: aa = a ; :: thesis:
set A = H .reachableFrom aa;
let x be Vertex of G; :: thesis:
assume A5: x in S ; :: thesis:
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:
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() )

let W be Walk of G; :: thesis:
assume that
A10: W is_Walk_from a,b and
A11: x in W .vertices() ; :: thesis:

A12: now :: thesis:

assume W .find x = 1 ; :: thesis:
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:

end;

consider k being odd Element of NAT such that
A13: k <= len W and
A14: W . k = x by A11, GLIB_001:87;
W .find (W . k) <= k by A13, GLIB_001:115;
then A15: W .find x <= len W by A13, A14, XXREAL_0:2;
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 A12, XXREAL_0:1;
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 A18, A16, GLIB_001:36;
assume A21: for y being Vertex of G holds
( not y in S \ {x} or not y in W .vertices() ) ; :: thesis:
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 )

let n be odd Nat; :: thesis:
assume A23: n <= j ; :: thesis:
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 A23, NAT_1:13;
then n + (- 1) < (j + 1) + (- 1) by XREAL_1:8;
then A25: (W .cut (1,j)) . (nu1 + 1) = W . (1 + nu1) by A16, A19, A20, A24, GLIB_001:36;

A26: (W .cut (1,j)) .vertices() c= W .vertices() by A18, A16, A19, GLIB_001:94;
A27: n in NAT by ORDINAL1:def 12;
then (W .cut (1,j)) . n in (W .cut (1,j)) .vertices() by A20, A23, GLIB_001:87;
then A28: not (W .cut (1,j)) . n in S \ {x} by A21, A26;
n < j + 1 by A23, NAT_1:13;
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 A5, ZFMISC_1:31;
then A31: S = {x} \/ (S \ {x}) by A30, XBOOLE_1:12;
A32: n <= len W by A16, A23, XXREAL_0:2;
assume (W .cut (1,j)) . n in S ; :: thesis:
then (W .cut (1,j)) . n in {x} by A28, A31, XBOOLE_0:def 3;
then n < W .find (W . n) by A25, A29, TARSKI:def 1;
hence contradiction by A27, A32, GLIB_001:115; :: thesis:

end;

hence ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n ) by A25; :: thesis:

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 A20, Th21;
W .first() = a by A10;
then (W .cut (1,j)) . ((2 * 0) + 1) = a by A17, A22;
then aa in HP .vertices() by A4, A17, A20, GLIB_001:87;
then A33: HP .vertices() c= H .reachableFrom aa by GLIB_002:13;
W .find x < (len W) + 1 by A15, NAT_1:13;
then A34: (W .find x) + (- 2) < ((len W) + 1) + (- 2) by XREAL_1:8;
(W .cut (1,j)) . j is Vertex of G by A20, GLIB_001:7;
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 A34, XXREAL_0:2;
then W . (j + 1) Joins Wj,W . (j + 2),G by A18, GLIB_001:def 3;
then W . (j + 1) Joins Wj,x,G by A11, GLIB_001:def 19;
then A35: Wj,x are_adjacent ;
(W .cut (1,j)) . j in HP .vertices() by A20, GLIB_001:87;
then W . j in HP .vertices() by A22;
hence contradiction by A8, A33, A35; :: thesis:

end;

A36: now :: thesis:

let W be Walk of G; :: thesis:
assume A37: W is_Walk_from a,b ; :: thesis:
consider y being Vertex of G such that
A38: y in S and
A39: y in W .vertices() by A1, A2, A37, Th70;

suppose y = x ; :: thesis:

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

end;

suppose A40: y <> x ; :: thesis:

take y = y; :: thesis:
not y in {x} by A40, TARSKI:def 1;
hence y in S \ {x} by A38, XBOOLE_0:def 5; :: thesis:
thus y in W .vertices() by A39; :: thesis:

end;

end;

end;

x in {x} by TARSKI:def 1;
then A41: S \ {x} <> S by A5, XBOOLE_0:def 5;
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: