let G be _Graph; :: thesis: for a, b being Vertex of st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of (the_Vertices_of G), holds
( a is Vertex of & b is Vertex of )
let a, b be Vertex of ; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b
for G2 being removeVertices of (the_Vertices_of G), holds
( a is Vertex of & b is Vertex of ) )
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 (the_Vertices_of G), holds
( a is Vertex of & b is Vertex of )
let S be VertexSeparator of a,b; :: thesis: for G2 being removeVertices of (the_Vertices_of G), holds
( a is Vertex of & b is Vertex of )
let G2 be removeVertices of (the_Vertices_of G),; :: thesis: ( a is Vertex of & b is Vertex of )
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 & b is Vertex of ) by A3, GLIB_000:def 39; :: thesis: verum