let G be _Graph; for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}
let a, b be Vertex of G; ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {} )
assume that
A1:
a <> b
and
A2:
not a,b are_adjacent
; for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}
let S be VertexSeparator of a,b; for G2 being removeVertices of G,S
for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}
let G2 be removeVertices of G,S; for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}
let a2 be Vertex of G2; (G2 .reachableFrom a2) /\ S = {}
set A = G2 .reachableFrom a2;
not a in S
by A1, A2, Def8;
then
a in (the_Vertices_of G) \ S
by XBOOLE_0:def 5;
then A3:
the_Vertices_of G2 = (the_Vertices_of G) \ S
by GLIB_000:def 37;
hence
(G2 .reachableFrom a2) /\ S = {}
by XBOOLE_0:def 1; verum