let G be _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds

for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b

let S be VertexSeparator of a,b; :: thesis: ( S = {} implies for W being Walk of G holds not W is_Walk_from a,b )

assume A3: S = {} ; :: thesis: for W being Walk of G holds not W is_Walk_from a,b

A4: the_Edges_of G c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;

A5: the_Vertices_of G c= the_Vertices_of G ;

set G2 = the removeVertices of G,S;

given W being Walk of G such that A6: W is_Walk_from a,b ; :: thesis: contradiction

the_Vertices_of the removeVertices of G,S = the_Vertices_of G by A3, GLIB_000:def 37;

then A7: W .vertices() c= the_Vertices_of the removeVertices of G,S ;

the removeVertices of G,S is inducedSubgraph of G, the_Vertices_of G, the_Edges_of G by A3, GLIB_000:34;

then the_Edges_of the removeVertices of G,S = the_Edges_of G by A5, A4, GLIB_000:def 37;

then W .edges() c= the_Edges_of the removeVertices of G,S ;

then reconsider W2 = W as Walk of the removeVertices of G,S by A7, GLIB_001:170;

W .last() = b by A6;

then A8: W2 .last() = b ;

W .first() = a by A6;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A8;

hence contradiction by A1, A2, Def8; :: thesis: verum

for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S = {} holds

for W being Walk of G holds not W is_Walk_from a,b

let S be VertexSeparator of a,b; :: thesis: ( S = {} implies for W being Walk of G holds not W is_Walk_from a,b )

assume A3: S = {} ; :: thesis: for W being Walk of G holds not W is_Walk_from a,b

A4: the_Edges_of G c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;

A5: the_Vertices_of G c= the_Vertices_of G ;

set G2 = the removeVertices of G,S;

given W being Walk of G such that A6: W is_Walk_from a,b ; :: thesis: contradiction

the_Vertices_of the removeVertices of G,S = the_Vertices_of G by A3, GLIB_000:def 37;

then A7: W .vertices() c= the_Vertices_of the removeVertices of G,S ;

the removeVertices of G,S is inducedSubgraph of G, the_Vertices_of G, the_Edges_of G by A3, GLIB_000:34;

then the_Edges_of the removeVertices of G,S = the_Edges_of G by A5, A4, GLIB_000:def 37;

then W .edges() c= the_Edges_of the removeVertices of G,S ;

then reconsider W2 = W as Walk of the removeVertices of G,S by A7, GLIB_001:170;

W .last() = b by A6;

then A8: W2 .last() = b ;

W .first() = a by A6;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A8;

hence contradiction by A1, A2, Def8; :: thesis: verum