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