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 Subset of (the_Vertices_of G); :: thesis:

hereby :: thesis:

assume A3: S is VertexSeparator of a,b ; :: thesis:
hence ( not a in S & not b in S ) by A1, A2, Def8; :: thesis:
then A4: not (the_Vertices_of G) \ S is empty by XBOOLE_0:def 5;
let W be Walk of G; :: thesis:
assume A5: W is_Walk_from a,b ; :: thesis:

now :: thesis:

assume A6: for x being Vertex of G holds
( not x in S or not x in W .vertices() ) ; :: thesis:
let G2 be removeVertices of G,S; :: thesis:
A7: the_Vertices_of G2 = (the_Vertices_of G) \ S by A4, GLIB_000:def 37;
then A8: the_Edges_of G2 = G .edgesBetween (the_Vertices_of G2) by GLIB_000:def 37;
A9: W .edges() c= G .edgesBetween (W .vertices()) by GLIB_001:109;

now :: thesis:

let x be object ; :: thesis:
assume A10: x in W .vertices() ; :: thesis:
not x in S by A6, A10;
hence x in the_Vertices_of G2 by A7, A10, XBOOLE_0:def 5; :: thesis:

end;

then A11: W .vertices() c= the_Vertices_of G2 ;
then G .edgesBetween (W .vertices()) c= G .edgesBetween (the_Vertices_of G2) by GLIB_000:36;
then W .edges() c= the_Edges_of G2 by A8, A9;
then reconsider W2 = W as Walk of G2 by A11, GLIB_001:170;
W .last() = b by A5;
then A12: W2 .last() = b ;
W .first() = a by A5;
then W2 .first() = a ;
then W2 is_Walk_from a,b by A12;
hence contradiction by A1, A2, A3, Def8; :: thesis:

end;

hence ex x being Vertex of G st
( x in S & x in W .vertices() ) ; :: thesis:

end;

assume that
A13: not a in S and
A14: not b in S and
A15: for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ; :: thesis:

now :: thesis:

let G2 be removeVertices of G,S; :: thesis:
given W being Walk of G2 such that A16: W is_Walk_from a,b ; :: thesis:
reconsider W2 = W as Walk of G by GLIB_001:167;
W .last() = b by A16;
then A17: W2 .last() = b ;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in W2 .vertices() ; :: thesis:
then ex n being odd Element of NAT st
( n <= len W & W . n = x ) by GLIB_001:87;
hence x in W .vertices() by GLIB_001:87; :: thesis:

end;

assume x in W .vertices() ; :: thesis:
then ex n being odd Element of NAT st
( n <= len W2 & W2 . n = x ) by GLIB_001:87;
hence x in W2 .vertices() by GLIB_001:87; :: thesis:

end;

then A18: W2 .vertices() = W .vertices() by TARSKI:2;
not (the_Vertices_of G) \ S is empty by A13, XBOOLE_0:def 5;
then the_Vertices_of G2 = (the_Vertices_of G) \ S by GLIB_000:def 37;
then A19: for x being Vertex of G holds
( not x in S or not x in W2 .vertices() ) by A18, XBOOLE_0:def 5;
W .first() = a by A16;
then W2 .first() = a ;
then W2 is_Walk_from a,b by A17;
hence contradiction by A15, A19; :: thesis:

end;

hence S is VertexSeparator of a,b by A1, A2, A13, A14, Def8; :: thesis: