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 st S is minimal holds
for H being removeVertices of (the_Vertices_of G),
for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
let a, b be Vertex of ; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of (the_Vertices_of G),
for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent ) )
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of (the_Vertices_of G),
for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for H being removeVertices of (the_Vertices_of G),
for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent ) )
assume A3: S is minimal ; :: thesis: for H being removeVertices of (the_Vertices_of G),
for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
reconsider S1 = S as VertexSeparator of b,a by A1, A2, Th70;
A4: S1 is minimal by A1, A2, A3, Th80;
let H be removeVertices of (the_Vertices_of G),; :: thesis: for aa being Vertex of st aa = b holds
for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
let aa be Vertex of ; :: thesis: ( aa = b implies for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent ) )
assume A5: aa = b ; :: thesis: for x being Vertex of st x in S holds
ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
let x be Vertex of ; :: thesis: ( x in S implies ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent ) )
assume x in S ; :: thesis: ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent )
hence ex y being Vertex of st
( y in H .reachableFrom aa & x,y are_adjacent ) by A1, A2, A5, A4, Th82; :: thesis: verum