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 A1: ( a <> b & 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 a in S & not b in S ) by A1, Def8;
then ( a in (the_Vertices_of G) \ S & b in (the_Vertices_of G) \ S ) by XBOOLE_0:def 5;
hence ( a is Vertex of G2 & b is Vertex of G2 ) by GLIB_000:def 39; :: thesis: verum