let G be _Graph; 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; ( 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
; 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; ( S = {} implies for W being Walk of G holds not W is_Walk_from a,b )
assume A3:
S = {}
; 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
; 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; verum