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

hence {} is VertexSeparator of a,b by A1, A2, A4, Def8; :: thesis: verum

{} 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 )

{} is Subset of (the_Vertices_of G)
by XBOOLE_1:2;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

end;( 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;

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

reconsider W2 = W as Walk of G by GLIB_001:167;

W .last() = b by A6;

then A7: W2 .last() = b ;

W .first() = a by A6;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A7;

hence contradiction by A3; :: thesis: verum

end;W .last() = b by A6;

then A7: W2 .last() = b ;

W .first() = a by A6;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A7;

hence contradiction by A3; :: thesis: verum

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:167;

A9: W .reverse() is_Walk_from a,b by A8, GLIB_001:23;

then (W .reverse()) .last() = b ;

then A10: W2 .last() = b ;

(W .reverse()) .first() = a by A9;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A10;

hence contradiction by A3; :: thesis: verum

end;reconsider W2 = W .reverse() as Walk of G by GLIB_001:167;

A9: W .reverse() is_Walk_from a,b by A8, GLIB_001:23;

then (W .reverse()) .last() = b ;

then A10: W2 .last() = b ;

(W .reverse()) .first() = a by A9;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A10;

hence contradiction by A3; :: thesis: verum

hence {} is VertexSeparator of a,b by A1, A2, A4, Def8; :: thesis: verum