set S = (the_Vertices_of G) \ {a,b};

a in {a,b} by TARSKI:def 2;

then A3: not a in (the_Vertices_of G) \ {a,b} by XBOOLE_0:def 5;

A4: for e being set holds not e Joins a,b,G by A2;

A5: for G2 being removeVertices of G,((the_Vertices_of G) \ {a,b})

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

then not b in (the_Vertices_of G) \ {a,b} by XBOOLE_0:def 5;

hence ex b_{1} being Subset of (the_Vertices_of G) st

( not a in b_{1} & not b in b_{1} & ( for G2 being removeVertices of G,b_{1}

for W being Walk of G2 holds not W is_Walk_from a,b ) ) by A3, A5; :: thesis: verum

a in {a,b} by TARSKI:def 2;

then A3: not a in (the_Vertices_of G) \ {a,b} by XBOOLE_0:def 5;

A4: for e being set holds not e Joins a,b,G by A2;

A5: for G2 being removeVertices of G,((the_Vertices_of G) \ {a,b})

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

proof

b in {a,b}
by TARSKI:def 2;
let G2 be removeVertices of G,((the_Vertices_of G) \ {a,b}); :: thesis: for W being Walk of G2 holds not W is_Walk_from a,b

let W be Walk of G2; :: thesis: not W is_Walk_from a,b

assume A6: W is_Walk_from a,b ; :: thesis: contradiction

then the_Vertices_of G2 = (the_Vertices_of G) \ ((the_Vertices_of G) \ {a,b}) by GLIB_000:def 37;

then the_Vertices_of G2 = (the_Vertices_of G) /\ {a,b} by XBOOLE_1:48;

then the_Vertices_of G2 = {a,b} by XBOOLE_1:28;

then for x being object holds

( x in W .vertices() iff x in {a,b} ) by A7;

then W .vertices() = {a,b} by TARSKI:2;

then W2 .vertices() = {a,b} by A9, TARSKI:2;

hence contradiction by A1, A4, Th22; :: thesis: verum

end;let W be Walk of G2; :: thesis: not W is_Walk_from a,b

assume A6: W is_Walk_from a,b ; :: thesis: contradiction

A7: now :: thesis: for x being set st x in {a,b} holds

x in W .vertices()

reconsider W2 = W as Walk of G by GLIB_001:167;x in W .vertices()

let x be set ; :: thesis: ( x in {a,b} implies x in W .vertices() )

assume A8: x in {a,b} ; :: thesis: x in W .vertices()

end;assume A8: x in {a,b} ; :: thesis: x in W .vertices()

now :: thesis: x in W .vertices() end;

hence
x in W .vertices()
; :: thesis: verumper cases
( x = a or x = b )
by A8, TARSKI:def 2;

end;

A9: 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() ) )

not (the_Vertices_of G) \ ((the_Vertices_of G) \ {a,b}) is empty
by A3, XBOOLE_0:def 5;( ( 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

then the_Vertices_of G2 = (the_Vertices_of G) \ ((the_Vertices_of G) \ {a,b}) by GLIB_000:def 37;

then the_Vertices_of G2 = (the_Vertices_of G) /\ {a,b} by XBOOLE_1:48;

then the_Vertices_of G2 = {a,b} by XBOOLE_1:28;

then for x being object holds

( x in W .vertices() iff x in {a,b} ) by A7;

then W .vertices() = {a,b} by TARSKI:2;

then W2 .vertices() = {a,b} by A9, TARSKI:2;

hence contradiction by A1, A4, Th22; :: thesis: verum

then not b in (the_Vertices_of G) \ {a,b} by XBOOLE_0:def 5;

hence ex b

( not a in b

for W being Walk of G2 holds not W is_Walk_from a,b ) ) by A3, A5; :: thesis: verum