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 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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() ) ; :: thesis: contradiction

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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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() ) ; :: thesis: contradiction

A8: now :: thesis: for W being Walk of G st W is_Walk_from a,b holds

ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

x in {x}
by TARSKI:def 1;ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() ) )

assume A9: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

consider y being Vertex of G such that

A10: y in S and

A11: y in W .vertices() by A1, A2, A9, Th70;

take y = y; :: thesis: ( y in S \ {x} & y in W .vertices() )

y <> x by A7, A9, A11;

then not y in {x} by TARSKI:def 1;

hence y in S \ {x} by A10, XBOOLE_0:def 5; :: thesis: y in W .vertices()

thus y in W .vertices() by A11; :: thesis: verum

end;( y in S \ {x} & y in W .vertices() ) )

assume A9: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

consider y being Vertex of G such that

A10: y in S and

A11: y in W .vertices() by A1, A2, A9, Th70;

take y = y; :: thesis: ( y in S \ {x} & y in W .vertices() )

y <> x by A7, A9, A11;

then not y in {x} by TARSKI:def 1;

hence y in S \ {x} by A10, XBOOLE_0:def 5; :: thesis: y in W .vertices()

thus y in W .vertices() by A11; :: thesis: verum

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; :: thesis: verum