let G be _Graph; for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being Subset of (the_Vertices_of G) holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )
let a, b be Vertex of G; ( a <> b & not a,b are_adjacent implies for S being Subset of (the_Vertices_of G) holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) ) )
assume that
A1:
a <> b
and
A2:
not a,b are_adjacent
; for S being Subset of (the_Vertices_of G) holds
( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )
let S be Subset of (the_Vertices_of G); ( S is VertexSeparator of a,b iff ( not a in S & not b in S & ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() ) ) ) )
assume that
A13:
not a in S
and
A14:
not b in S
and
A15:
for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S & x in W .vertices() )
; S is VertexSeparator of a,b
hence
S is VertexSeparator of a,b
by A1, A2, A13, A14, Def8; verum