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 = a 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 = a 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 = a 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 = a 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 = a 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 H be removeVertices of G,S; :: thesis: for aa being Vertex of H st aa = a 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 = a 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 A4: aa = a ; :: 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 )

set A = H .reachableFrom aa;

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 A5: x in S ; :: thesis: ex y being Vertex of G st

( y in H .reachableFrom aa & x,y are_adjacent )

set T = S \ {x};

A6: S \ {x} c= S by XBOOLE_1:36;

then A7: not b in S \ {x} by A1, A2, Def8;

assume A8: for y being Vertex of G holds

( not y in H .reachableFrom aa or not x,y are_adjacent ) ; :: thesis: contradiction

A9: for W being Walk of G st W is_Walk_from a,b & x in W .vertices() holds

ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

then A41: S \ {x} <> S by A5, XBOOLE_0:def 5;

not a in S \ {x} by A1, A2, A6, Def8;

then S \ {x} is VertexSeparator of a,b by A1, A2, A7, A36, Th70;

hence contradiction by A3, A41, A6; :: thesis: verum

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 = a 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 = a 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 = a 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 = a 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 = a 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 H be removeVertices of G,S; :: thesis: for aa being Vertex of H st aa = a 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 = a 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 A4: aa = a ; :: 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 )

set A = H .reachableFrom aa;

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 A5: x in S ; :: thesis: ex y being Vertex of G st

( y in H .reachableFrom aa & x,y are_adjacent )

set T = S \ {x};

A6: S \ {x} c= S by XBOOLE_1:36;

then A7: not b in S \ {x} by A1, A2, Def8;

assume A8: for y being Vertex of G holds

( not y in H .reachableFrom aa or not x,y are_adjacent ) ; :: thesis: contradiction

A9: for W being Walk of G st W is_Walk_from a,b & x in W .vertices() holds

ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

proof

let W be Walk of G; :: thesis: ( W is_Walk_from a,b & x in W .vertices() implies ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() ) )

assume that

A10: W is_Walk_from a,b and

A11: x in W .vertices() ; :: thesis: ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

A13: k <= len W and

A14: W . k = x by A11, GLIB_001:87;

W .find (W . k) <= k by A13, GLIB_001:115;

then A15: W .find x <= len W by A13, A14, XXREAL_0:2;

then A16: (W .find x) + (- 2) <= (len W) + 0 by XREAL_1:7;

0 + 1 <= W .find x by ABIAN:12;

then (2 * 0) + 1 < W .find x by A12, XXREAL_0:1;

then (2 * 1) + 1 <= W .find x by Th4;

then A17: 3 + (- 2) <= (W .find x) + (- 2) by XREAL_1:7;

then A18: (W .find x) - 2 is Element of NAT by INT_1:3;

then reconsider j = (W .find x) - (2 * 1) as odd Nat ;

set P = W .cut (1,j);

A19: (2 * 0) + 1 <= j by A17;

then A20: ((len (W .cut (1,j))) + 1) + (- 1) = (j + 1) + (- 1) by A18, A16, GLIB_001:36;

assume A21: for y being Vertex of G holds

( not y in S \ {x} or not y in W .vertices() ) ; :: thesis: contradiction

A22: for n being odd Nat st n <= j holds

( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )

not (W .cut (1,j)) . n in S ;

then reconsider HP = W .cut (1,j) as Walk of H by A20, Th21;

W .first() = a by A10;

then (W .cut (1,j)) . ((2 * 0) + 1) = a by A17, A22;

then aa in HP .vertices() by A4, A17, A20, GLIB_001:87;

then A33: HP .vertices() c= H .reachableFrom aa by GLIB_002:13;

W .find x < (len W) + 1 by A15, NAT_1:13;

then A34: (W .find x) + (- 2) < ((len W) + 1) + (- 2) by XREAL_1:8;

(W .cut (1,j)) . j is Vertex of G by A20, GLIB_001:7;

then reconsider Wj = W . j as Vertex of G by A22;

(len W) + (- 1) < (len W) + 0 by XREAL_1:8;

then j < len W by A34, XXREAL_0:2;

then W . (j + 1) Joins Wj,W . (j + 2),G by A18, GLIB_001:def 3;

then W . (j + 1) Joins Wj,x,G by A11, GLIB_001:def 19;

then A35: Wj,x are_adjacent ;

(W .cut (1,j)) . j in HP .vertices() by A20, GLIB_001:87;

then W . j in HP .vertices() by A22;

hence contradiction by A8, A33, A35; :: thesis: verum

end;( y in S \ {x} & y in W .vertices() ) )

assume that

A10: W is_Walk_from a,b and

A11: x in W .vertices() ; :: thesis: ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

A12: now :: thesis: not W .find x = 1

consider k being odd Element of NAT such that assume
W .find x = 1
; :: thesis: contradiction

then W . (W .find x) = W .first() ;

then W . (W .find x) = a by A10;

then not W . (W .find x) in S by A1, A2, Def8;

hence contradiction by A5, A11, GLIB_001:def 19; :: thesis: verum

end;then W . (W .find x) = W .first() ;

then W . (W .find x) = a by A10;

then not W . (W .find x) in S by A1, A2, Def8;

hence contradiction by A5, A11, GLIB_001:def 19; :: thesis: verum

A13: k <= len W and

A14: W . k = x by A11, GLIB_001:87;

W .find (W . k) <= k by A13, GLIB_001:115;

then A15: W .find x <= len W by A13, A14, XXREAL_0:2;

then A16: (W .find x) + (- 2) <= (len W) + 0 by XREAL_1:7;

0 + 1 <= W .find x by ABIAN:12;

then (2 * 0) + 1 < W .find x by A12, XXREAL_0:1;

then (2 * 1) + 1 <= W .find x by Th4;

then A17: 3 + (- 2) <= (W .find x) + (- 2) by XREAL_1:7;

then A18: (W .find x) - 2 is Element of NAT by INT_1:3;

then reconsider j = (W .find x) - (2 * 1) as odd Nat ;

set P = W .cut (1,j);

A19: (2 * 0) + 1 <= j by A17;

then A20: ((len (W .cut (1,j))) + 1) + (- 1) = (j + 1) + (- 1) by A18, A16, GLIB_001:36;

assume A21: for y being Vertex of G holds

( not y in S \ {x} or not y in W .vertices() ) ; :: thesis: contradiction

A22: for n being odd Nat st n <= j holds

( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )

proof

then
for n being odd Nat st n <= j holds
let n be odd Nat; :: thesis: ( n <= j implies ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n ) )

assume A23: n <= j ; :: thesis: ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )

1 <= n by ABIAN:12;

then 1 + (- 1) <= n + (- 1) by XREAL_1:7;

then A24: n - 1 is Element of NAT by INT_1:3;

then reconsider nu1 = n - 1 as Nat ;

n < j + 1 by A23, NAT_1:13;

then n + (- 1) < (j + 1) + (- 1) by XREAL_1:8;

then A25: (W .cut (1,j)) . (nu1 + 1) = W . (1 + nu1) by A16, A19, A20, A24, GLIB_001:36;

end;assume A23: n <= j ; :: thesis: ( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )

1 <= n by ABIAN:12;

then 1 + (- 1) <= n + (- 1) by XREAL_1:7;

then A24: n - 1 is Element of NAT by INT_1:3;

then reconsider nu1 = n - 1 as Nat ;

n < j + 1 by A23, NAT_1:13;

then n + (- 1) < (j + 1) + (- 1) by XREAL_1:8;

then A25: (W .cut (1,j)) . (nu1 + 1) = W . (1 + nu1) by A16, A19, A20, A24, GLIB_001:36;

now :: thesis: not (W .cut (1,j)) . n in S

hence
( not (W .cut (1,j)) . n in S & (W .cut (1,j)) . n = W . n )
by A25; :: thesis: verumA26:
(W .cut (1,j)) .vertices() c= W .vertices()
by A18, A16, A19, GLIB_001:94;

A27: n in NAT by ORDINAL1:def 12;

then (W .cut (1,j)) . n in (W .cut (1,j)) .vertices() by A20, A23, GLIB_001:87;

then A28: not (W .cut (1,j)) . n in S \ {x} by A21, A26;

n < j + 1 by A23, NAT_1:13;

then A29: n + 0 < (j + 1) + 1 by XREAL_1:8;

A30: S \/ {x} = {x} \/ (S \ {x}) by XBOOLE_1:39;

{x} c= S by A5, ZFMISC_1:31;

then A31: S = {x} \/ (S \ {x}) by A30, XBOOLE_1:12;

A32: n <= len W by A16, A23, XXREAL_0:2;

assume (W .cut (1,j)) . n in S ; :: thesis: contradiction

then (W .cut (1,j)) . n in {x} by A28, A31, XBOOLE_0:def 3;

then n < W .find (W . n) by A25, A29, TARSKI:def 1;

hence contradiction by A27, A32, GLIB_001:115; :: thesis: verum

end;A27: n in NAT by ORDINAL1:def 12;

then (W .cut (1,j)) . n in (W .cut (1,j)) .vertices() by A20, A23, GLIB_001:87;

then A28: not (W .cut (1,j)) . n in S \ {x} by A21, A26;

n < j + 1 by A23, NAT_1:13;

then A29: n + 0 < (j + 1) + 1 by XREAL_1:8;

A30: S \/ {x} = {x} \/ (S \ {x}) by XBOOLE_1:39;

{x} c= S by A5, ZFMISC_1:31;

then A31: S = {x} \/ (S \ {x}) by A30, XBOOLE_1:12;

A32: n <= len W by A16, A23, XXREAL_0:2;

assume (W .cut (1,j)) . n in S ; :: thesis: contradiction

then (W .cut (1,j)) . n in {x} by A28, A31, XBOOLE_0:def 3;

then n < W .find (W . n) by A25, A29, TARSKI:def 1;

hence contradiction by A27, A32, GLIB_001:115; :: thesis: verum

not (W .cut (1,j)) . n in S ;

then reconsider HP = W .cut (1,j) as Walk of H by A20, Th21;

W .first() = a by A10;

then (W .cut (1,j)) . ((2 * 0) + 1) = a by A17, A22;

then aa in HP .vertices() by A4, A17, A20, GLIB_001:87;

then A33: HP .vertices() c= H .reachableFrom aa by GLIB_002:13;

W .find x < (len W) + 1 by A15, NAT_1:13;

then A34: (W .find x) + (- 2) < ((len W) + 1) + (- 2) by XREAL_1:8;

(W .cut (1,j)) . j is Vertex of G by A20, GLIB_001:7;

then reconsider Wj = W . j as Vertex of G by A22;

(len W) + (- 1) < (len W) + 0 by XREAL_1:8;

then j < len W by A34, XXREAL_0:2;

then W . (j + 1) Joins Wj,W . (j + 2),G by A18, GLIB_001:def 3;

then W . (j + 1) Joins Wj,x,G by A11, GLIB_001:def 19;

then A35: Wj,x are_adjacent ;

(W .cut (1,j)) . j in HP .vertices() by A20, GLIB_001:87;

then W . j in HP .vertices() by A22;

hence contradiction by A8, A33, A35; :: thesis: verum

A36: now :: thesis: for W being Walk of G st W is_Walk_from a,b holds

ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

x in {x}
by TARSKI:def 1;ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() )

let W be Walk of G; :: thesis: ( W is_Walk_from a,b implies ex y being Vertex of G st

( b_{2} in S \ {x} & b_{2} in y .vertices() ) )

assume A37: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st

( b_{2} in S \ {x} & b_{2} in y .vertices() )

consider y being Vertex of G such that

A38: y in S and

A39: y in W .vertices() by A1, A2, A37, Th70;

end;( b

assume A37: W is_Walk_from a,b ; :: thesis: ex y being Vertex of G st

( b

consider y being Vertex of G such that

A38: y in S and

A39: y in W .vertices() by A1, A2, A37, Th70;

per cases
( y = x or y <> x )
;

end;

suppose
y = x
; :: thesis: ex y being Vertex of G st

( b_{2} in S \ {x} & b_{2} in y .vertices() )

( b

hence
ex y being Vertex of G st

( y in S \ {x} & y in W .vertices() ) by A9, A37, A39; :: thesis: verum

end;( y in S \ {x} & y in W .vertices() ) by A9, A37, A39; :: thesis: verum

suppose A40:
y <> x
; :: thesis: ex y being Vertex of G st

( b_{2} in S \ {x} & b_{2} in y .vertices() )

( b

take y = y; :: thesis: ( y in S \ {x} & y in W .vertices() )

not y in {x} by A40, TARSKI:def 1;

hence y in S \ {x} by A38, XBOOLE_0:def 5; :: thesis: y in W .vertices()

thus y in W .vertices() by A39; :: thesis: verum

end;not y in {x} by A40, TARSKI:def 1;

hence y in S \ {x} by A38, XBOOLE_0:def 5; :: thesis: y in W .vertices()

thus y in W .vertices() by A39; :: thesis: verum

then A41: S \ {x} <> S by A5, XBOOLE_0:def 5;

not a in S \ {x} by A1, A2, A6, Def8;

then S \ {x} is VertexSeparator of a,b by A1, A2, A7, A36, Th70;

hence contradiction by A3, A41, A6; :: thesis: verum