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 holds

( a is Vertex of G2 & b is Vertex of G2 )

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 holds

( a is Vertex of G2 & b is Vertex of G2 ) )

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 holds

( a is Vertex of G2 & b is Vertex of G2 )

let S be VertexSeparator of a,b; :: thesis: for G2 being removeVertices of G,S holds

( a is Vertex of G2 & b is Vertex of G2 )

let G2 be removeVertices of G,S; :: thesis: ( a is Vertex of G2 & b is Vertex of G2 )

not b in S by A1, A2, Def8;

then A3: b in (the_Vertices_of G) \ S by XBOOLE_0:def 5;

not a in S by A1, A2, Def8;

then a in (the_Vertices_of G) \ S by XBOOLE_0:def 5;

hence ( a is Vertex of G2 & b is Vertex of G2 ) by A3, GLIB_000:def 37; :: thesis: verum

for S being VertexSeparator of a,b

for G2 being removeVertices of G,S holds

( a is Vertex of G2 & b is Vertex of G2 )

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 holds

( a is Vertex of G2 & b is Vertex of G2 ) )

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 holds

( a is Vertex of G2 & b is Vertex of G2 )

let S be VertexSeparator of a,b; :: thesis: for G2 being removeVertices of G,S holds

( a is Vertex of G2 & b is Vertex of G2 )

let G2 be removeVertices of G,S; :: thesis: ( a is Vertex of G2 & b is Vertex of G2 )

not b in S by A1, A2, Def8;

then A3: b in (the_Vertices_of G) \ S by XBOOLE_0:def 5;

not a in S by A1, A2, Def8;

then a in (the_Vertices_of G) \ S by XBOOLE_0:def 5;

hence ( a is Vertex of G2 & b is Vertex of G2 ) by A3, GLIB_000:def 37; :: thesis: verum