let G be _Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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() ) ) ) )

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() ) ; :: thesis: S is VertexSeparator of a,b

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

hereby :: thesis: ( 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() ) ) implies S is VertexSeparator of a,b )

assume that ex x being Vertex of G st

( x in S & x in W .vertices() ) ) implies S is VertexSeparator of a,b )

assume A3:
S is VertexSeparator of a,b
; :: thesis: ( 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() ) ) )

hence ( not a in S & not b in S ) by A1, A2, Def8; :: thesis: 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() )

then A4: not (the_Vertices_of G) \ S is empty by XBOOLE_0:def 5;

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

( x in S & x in W .vertices() ) )

assume A5: W is_Walk_from a,b ; :: thesis: ex x being Vertex of G st

( x in S & x in W .vertices() )

( x in S & x in W .vertices() ) ; :: thesis: verum

end;ex x being Vertex of G st

( x in S & x in W .vertices() ) ) )

hence ( not a in S & not b in S ) by A1, A2, Def8; :: thesis: 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() )

then A4: not (the_Vertices_of G) \ S is empty by XBOOLE_0:def 5;

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

( x in S & x in W .vertices() ) )

assume A5: W is_Walk_from a,b ; :: thesis: ex x being Vertex of G st

( x in S & x in W .vertices() )

now :: thesis: ( ( for x being Vertex of G holds

( not x in S or not x in W .vertices() ) ) implies for G2 being removeVertices of G,S holds contradiction )

hence
ex x being Vertex of G st ( not x in S or not x in W .vertices() ) ) implies for G2 being removeVertices of G,S holds contradiction )

assume A6:
for x being Vertex of G holds

( not x in S or not x in W .vertices() ) ; :: thesis: for G2 being removeVertices of G,S holds contradiction

let G2 be removeVertices of G,S; :: thesis: contradiction

A7: the_Vertices_of G2 = (the_Vertices_of G) \ S by A4, GLIB_000:def 37;

then A8: the_Edges_of G2 = G .edgesBetween (the_Vertices_of G2) by GLIB_000:def 37;

A9: W .edges() c= G .edgesBetween (W .vertices()) by GLIB_001:109;

then G .edgesBetween (W .vertices()) c= G .edgesBetween (the_Vertices_of G2) by GLIB_000:36;

then W .edges() c= the_Edges_of G2 by A8, A9;

then reconsider W2 = W as Walk of G2 by A11, GLIB_001:170;

W .last() = b by A5;

then A12: W2 .last() = b ;

W .first() = a by A5;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A12;

hence contradiction by A1, A2, A3, Def8; :: thesis: verum

end;( not x in S or not x in W .vertices() ) ; :: thesis: for G2 being removeVertices of G,S holds contradiction

let G2 be removeVertices of G,S; :: thesis: contradiction

A7: the_Vertices_of G2 = (the_Vertices_of G) \ S by A4, GLIB_000:def 37;

then A8: the_Edges_of G2 = G .edgesBetween (the_Vertices_of G2) by GLIB_000:def 37;

A9: W .edges() c= G .edgesBetween (W .vertices()) by GLIB_001:109;

now :: thesis: for x being object st x in W .vertices() holds

x in the_Vertices_of G2

then A11:
W .vertices() c= the_Vertices_of G2
;x in the_Vertices_of G2

let x be object ; :: thesis: ( x in W .vertices() implies x in the_Vertices_of G2 )

assume A10: x in W .vertices() ; :: thesis: x in the_Vertices_of G2

not x in S by A6, A10;

hence x in the_Vertices_of G2 by A7, A10, XBOOLE_0:def 5; :: thesis: verum

end;assume A10: x in W .vertices() ; :: thesis: x in the_Vertices_of G2

not x in S by A6, A10;

hence x in the_Vertices_of G2 by A7, A10, XBOOLE_0:def 5; :: thesis: verum

then G .edgesBetween (W .vertices()) c= G .edgesBetween (the_Vertices_of G2) by GLIB_000:36;

then W .edges() c= the_Edges_of G2 by A8, A9;

then reconsider W2 = W as Walk of G2 by A11, GLIB_001:170;

W .last() = b by A5;

then A12: W2 .last() = b ;

W .first() = a by A5;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A12;

hence contradiction by A1, A2, A3, Def8; :: thesis: verum

( x in S & x in W .vertices() ) ; :: thesis: verum

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() ) ; :: thesis: S is VertexSeparator of a,b

now :: thesis: for G2 being removeVertices of G,S

for W being Walk of G2 holds not W is_Walk_from a,b

hence
S is VertexSeparator of a,b
by A1, A2, A13, A14, Def8; :: thesis: verumfor W being Walk of G2 holds not W is_Walk_from a,b

let G2 be removeVertices of G,S; :: thesis: for W being Walk of G2 holds not W is_Walk_from a,b

given W being Walk of G2 such that A16: W is_Walk_from a,b ; :: thesis: contradiction

reconsider W2 = W as Walk of G by GLIB_001:167;

W .last() = b by A16;

then A17: W2 .last() = b ;

not (the_Vertices_of G) \ S is empty by A13, XBOOLE_0:def 5;

then the_Vertices_of G2 = (the_Vertices_of G) \ S by GLIB_000:def 37;

then A19: for x being Vertex of G holds

( not x in S or not x in W2 .vertices() ) by A18, XBOOLE_0:def 5;

W .first() = a by A16;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A17;

hence contradiction by A15, A19; :: thesis: verum

end;given W being Walk of G2 such that A16: W is_Walk_from a,b ; :: thesis: contradiction

reconsider W2 = W as Walk of G by GLIB_001:167;

W .last() = b by A16;

then A17: W2 .last() = b ;

now :: thesis: for x being object holds

( ( x in W2 .vertices() implies x in W .vertices() ) & ( x in W .vertices() implies x in W2 .vertices() ) )

then A18:
W2 .vertices() = W .vertices()
by TARSKI:2;( ( x in W2 .vertices() implies x in W .vertices() ) & ( x in W .vertices() implies x in W2 .vertices() ) )

let x be object ; :: thesis: ( ( x in W2 .vertices() implies x in W .vertices() ) & ( x in W .vertices() implies x in W2 .vertices() ) )

then ex n being odd Element of NAT st

( n <= len W2 & W2 . n = x ) by GLIB_001:87;

hence x in W2 .vertices() by GLIB_001:87; :: thesis: verum

end;hereby :: thesis: ( x in W .vertices() implies x in W2 .vertices() )

assume
x in W .vertices()
; :: thesis: x in W2 .vertices() assume
x in W2 .vertices()
; :: thesis: x in W .vertices()

then ex n being odd Element of NAT st

( n <= len W & W . n = x ) by GLIB_001:87;

hence x in W .vertices() by GLIB_001:87; :: thesis: verum

end;then ex n being odd Element of NAT st

( n <= len W & W . n = x ) by GLIB_001:87;

hence x in W .vertices() by GLIB_001:87; :: thesis: verum

then ex n being odd Element of NAT st

( n <= len W2 & W2 . n = x ) by GLIB_001:87;

hence x in W2 .vertices() by GLIB_001:87; :: thesis: verum

not (the_Vertices_of G) \ S is empty by A13, XBOOLE_0:def 5;

then the_Vertices_of G2 = (the_Vertices_of G) \ S by GLIB_000:def 37;

then A19: for x being Vertex of G holds

( not x in S or not x in W2 .vertices() ) by A18, XBOOLE_0:def 5;

W .first() = a by A16;

then W2 .first() = a ;

then W2 is_Walk_from a,b by A17;

hence contradiction by A15, A19; :: thesis: verum