let G be _Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}

let a2 be Vertex of G2; :: thesis: (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;

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}

let a2 be Vertex of G2; :: thesis: (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;

now :: thesis: for x being object holds not x in (G2 .reachableFrom a2) /\ S

hence
(G2 .reachableFrom a2) /\ S = {}
by XBOOLE_0:def 1; :: thesis: verumlet x be object ; :: thesis: not x in (G2 .reachableFrom a2) /\ S

assume A4: x in (G2 .reachableFrom a2) /\ S ; :: thesis: contradiction

A5: x in S by A4, XBOOLE_0:def 4;

x in G2 .reachableFrom a2 by A4, XBOOLE_0:def 4;

hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;assume A4: x in (G2 .reachableFrom a2) /\ S ; :: thesis: contradiction

A5: x in S by A4, XBOOLE_0:def 4;

x in G2 .reachableFrom a2 by A4, XBOOLE_0:def 4;

hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum