set S = () \ {a,b};
a in {a,b} by TARSKI:def 2;
then A3: not a in () \ {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,(() \ {a,b})
for W being Walk of G2 holds not W is_Walk_from a,b
proof
let G2 be removeVertices 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()
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() ) end;
assume x in W .vertices() ; :: thesis:
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) \ (() \ {a,b}) is empty by ;
then the_Vertices_of G2 = () \ (() \ {a,b}) by GLIB_000:def 37;
then the_Vertices_of G2 = () /\ {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 ;
hence contradiction by A1, A4, Th22; :: thesis: verum
end;
b in {a,b} by TARSKI:def 2;
then not b in () \ {a,b} by XBOOLE_0:def 5;
hence ex b1 being Subset of () st
( not a in b1 & not b in b1 & ( for G2 being removeVertices of G,b1
for W being Walk of G2 holds not W is_Walk_from a,b ) ) by A3, A5; :: thesis: verum