let G be _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent & ( for W being Walk of G holds not W is_Walk_from a,b ) holds
{} is VertexSeparator of a,b
let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent & ( for W being Walk of G holds not W is_Walk_from a,b ) implies {} is VertexSeparator of a,b )
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: ( ex W being Walk of G st W is_Walk_from a,b or {} is VertexSeparator of a,b )
assume A3: for W being Walk of G holds not W is_Walk_from a,b ; :: thesis: {} is VertexSeparator of a,b

A4: now

let G2 be removeVertices of G,{} ; :: thesis: for W being Walk of G2 holds
( not W is_Walk_from a,b & not W is_Walk_from b,a )
given W being Walk of G2 such that A5: ( W is_Walk_from a,b or W is_Walk_from b,a ) ; :: thesis: contradiction

per cases ( W is_Walk_from a,b or W is_Walk_from b,a ) by A5;

suppose A6: W is_Walk_from a,b ; :: thesis: contradiction

reconsider W2 = W as Walk of G by GLIB_001:168;
W .last() = b by A6, GLIB_001:def 23;
then A7: W2 .last() = b ;
W .first() = a by A6, GLIB_001:def 23;
then W2 .first() = a ;
then W2 is_Walk_from a,b by A7, GLIB_001:def 23;
hence contradiction by A3; :: thesis: verum

end;

suppose A8: W is_Walk_from b,a ; :: thesis: contradiction

set P = W .reverse() ;
reconsider W2 = W .reverse() as Walk of G by GLIB_001:168;
A9: W .reverse() is_Walk_from a,b by A8, GLIB_001:24;
then (W .reverse() ) .last() = b by GLIB_001:def 23;
then A10: W2 .last() = b ;
(W .reverse() ) .first() = a by A9, GLIB_001:def 23;
then W2 .first() = a ;
then W2 is_Walk_from a,b by A10, GLIB_001:def 23;
hence contradiction by A3; :: thesis: verum

end;

end;

end;

{} is Subset of (the_Vertices_of G) by XBOOLE_1:2;
hence {} is VertexSeparator of a,b by A1, A2, A4, Def8; :: thesis: verum