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

proof

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

A7: now :: thesis: for x being set st x in {a,b} holds
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()

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

per cases ( x = a or x = b ) by A8, TARSKI:def 2;

suppose x = a ; :: thesis: x in W .vertices()

then x = W .first() by A6;
hence x in W .vertices() by GLIB_001:88; :: thesis: verum

end;

suppose x = b ; :: thesis: x in W .vertices()

then x = W .last() by A6;
hence x in W .vertices() by GLIB_001:88; :: thesis: verum

end;

end;

end;

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

end;

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

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

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

hereby :: thesis: ( x in W .vertices() implies 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;

assume x in W .vertices() ; :: thesis: 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;

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

b in {a,b} by TARSKI:def 2;
then not b in (the_Vertices_of G) \ {a,b} by XBOOLE_0:def 5;
hence ex b₁ being Subset of (the_Vertices_of G) st
( not a in b₁ & not b in b₁ & ( for G2 being removeVertices of G,b₁
for W being Walk of G2 holds not W is_Walk_from a,b ) ) by A3, A5; :: thesis: verum