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 :: thesis: for G2 being removeVertices of G,{}
for W being Walk of G2 holds
( not W is_Walk_from a,b & not W is_Walk_from b,a )
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;
end;
end;
{} is Subset of () by XBOOLE_1:2;
hence {} is VertexSeparator of a,b by A1, A2, A4, Def8; :: thesis: verum