let G be _finite chordal _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 a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,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 a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,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 a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent )
let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent ) )
assume A3: S is minimal ; :: thesis: for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent )
let H be removeVertices of G,S; :: thesis: for a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent )
let a1 be Vertex of H; :: thesis: ( a = a1 implies for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent ) )
assume a = a1 ; :: thesis: for x, y being Vertex of G st x in S & y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent )
then consider c being Vertex of G such that
A4: c in H .reachableFrom a1 and
A5: for x being Vertex of G st x in S holds
c,x are_adjacent by A1, A2, A3, Th99;
let x, y be Vertex of G; :: thesis: ( x in S & y in S implies ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent ) )
assume that
A6: x in S and
A7: y in S ; :: thesis: ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent )
A8: c,y are_adjacent by A7, A5;
c,x are_adjacent by A6, A5;
hence ex c being Vertex of G st
( c in H .reachableFrom a1 & c,x are_adjacent & c,y are_adjacent ) by A4, A8; :: thesis: verum