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

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