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 is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let a, b be Vertex of G; ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume that
A1:
a <> b
and
A2:
not a,b are_adjacent
; for S being VertexSeparator of a,b st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let S be VertexSeparator of a,b; ( S is minimal implies for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume A3:
S is minimal
; for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
let x be Vertex of G; ( x in S implies ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() ) )
assume A4:
x in S
; ex W being Walk of G st
( W is_Walk_from a,b & x in W .vertices() )
set T = S \ {x};
A5:
S \ {x} c= S
by XBOOLE_1:36;
then A6:
not b in S \ {x}
by A1, A2, Def8;
assume A7:
for W being Walk of G holds
( not W is_Walk_from a,b or not x in W .vertices() )
; contradiction
x in {x}
by TARSKI:def 1;
then A12:
S \ {x} <> S
by A4, XBOOLE_0:def 5;
not a in S \ {x}
by A1, A2, A5, Def8;
then
S \ {x} is VertexSeparator of a,b
by A1, A2, A6, A8, Th70;
hence
contradiction
by A3, A12, A5; verum