let G be _Graph; :: thesis:
let a, b be Vertex of G; :: thesis:
assume A1: ( a <> b & not a,b are_adjacent ) ; :: thesis:
let S be Subset of (the_Vertices_of G); :: thesis:

hereby :: thesis:

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

assume A5: 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:
A6: the_Vertices_of G2 = (the_Vertices_of G) \ S by A3, GLIB_000:def 39;
then A7: the_Edges_of G2 = G .edgesBetween (the_Vertices_of G2) by GLIB_000:def 39;

let x be set ; :: thesis:
assume A8: x in W .vertices() ; :: thesis:
( x in the_Vertices_of G & not x in S ) by A5, A8;
hence x in the_Vertices_of G2 by A6, XBOOLE_0:def 5; :: thesis:

end;

then A9: W .vertices() c= the_Vertices_of G2 by TARSKI:def 3;
A10: W .edges() c= G .edgesBetween (W .vertices() ) by GLIB_001:110;
G .edgesBetween (W .vertices() ) c= G .edgesBetween (the_Vertices_of G2) by A9, GLIB_000:39;
then W .edges() c= the_Edges_of G2 by A7, A10, XBOOLE_1:1;
then reconsider W2 = W as Walk of G2 by A9, GLIB_001:171;
( W .first() = a & W .last() = b ) by A4, GLIB_001:def 23;
then ( W2 .first() = a & W2 .last() = b ) ;
then W2 is_Walk_from a,b by GLIB_001:def 23;
hence contradiction by A1, A2, Def8; :: thesis:

end;

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

end;

assume A11: ( not a in S & not b in S & ( 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:

let G2 be removeVertices of G,S; :: thesis:
not (the_Vertices_of G) \ S is empty by A11, XBOOLE_0:def 5;
then A12: the_Vertices_of G2 = (the_Vertices_of G) \ S by GLIB_000:def 39;
given W being Walk of G2 such that A13: W is_Walk_from a,b ; :: thesis:
reconsider W2 = W as Walk of G by GLIB_001:168;
( W .first() = a & W .last() = b ) by A13, GLIB_001:def 23;
then ( W2 .first() = a & W2 .last() = b ) ;
then A14: W2 is_Walk_from a,b by GLIB_001:def 23;

let x be set ; :: 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:88;
hence x in W .vertices() by GLIB_001:88; :: 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:88;
hence x in W2 .vertices() by GLIB_001:88; :: thesis:

end;

then W2 .vertices() = W .vertices() by TARSKI:2;
then for x being Vertex of G holds
( not x in S or not x in W2 .vertices() ) by A12, XBOOLE_0:def 5;
hence contradiction by A11, A14; :: thesis:

end;

hence S is VertexSeparator of a,b by A1, A11, Def8; :: thesis: