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