let G be _Graph; :: thesis: ( G is connected implies for A, B being non empty Subset of (the_Vertices_of G) st A misses B holds

ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) )

assume A1: G is connected ; :: thesis: for A, B being non empty Subset of (the_Vertices_of G) st A misses B holds

ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) )

let A, B be non empty Subset of (the_Vertices_of G); :: thesis: ( A misses B implies ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) )

assume A2: A misses B ; :: thesis: ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) )

set X = { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } ;

A3: { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } c= NAT

A4: b in B by XBOOLE_0:def 1;

reconsider b = b as Vertex of G by A4;

consider a being object such that

A5: a in A by XBOOLE_0:def 1;

reconsider a = a as Vertex of G by A5;

consider W being Walk of G such that

A6: W is_Walk_from a,b by A1;

consider W2 being Path of G such that

A7: W2 is_Walk_from W .first() ,W .last() and

W2 is minlength by Th38;

W .last() = b by A6;

then A8: W2 .last() in B by A4, A7;

W .first() = a by A6;

then W2 .first() in A by A5, A7;

then len W2 in { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } by A8;

then reconsider X = { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } as non empty Subset of NAT by A3;

min X in X by XXREAL_2:def 7;

then consider M being Path of G such that

A9: len M = min X and

A10: M .first() in A and

A11: M .last() in B ;

then not M is trivial by GLIB_001:127;

hence ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) by A10, A11, A14, A15; :: thesis: verum

ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) )

assume A1: G is connected ; :: thesis: for A, B being non empty Subset of (the_Vertices_of G) st A misses B holds

ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) )

let A, B be non empty Subset of (the_Vertices_of G); :: thesis: ( A misses B implies ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) )

assume A2: A misses B ; :: thesis: ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) )

set X = { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } ;

A3: { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } c= NAT

proof

consider b being object such that
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } or x in NAT )

assume x in { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } ; :: thesis: x in NAT

then ex P being Path of G st

( x = len P & P .first() in A & P .last() in B ) ;

hence x in NAT ; :: thesis: verum

end;assume x in { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } ; :: thesis: x in NAT

then ex P being Path of G st

( x = len P & P .first() in A & P .last() in B ) ;

hence x in NAT ; :: thesis: verum

A4: b in B by XBOOLE_0:def 1;

reconsider b = b as Vertex of G by A4;

consider a being object such that

A5: a in A by XBOOLE_0:def 1;

reconsider a = a as Vertex of G by A5;

consider W being Walk of G such that

A6: W is_Walk_from a,b by A1;

consider W2 being Path of G such that

A7: W2 is_Walk_from W .first() ,W .last() and

W2 is minlength by Th38;

W .last() = b by A6;

then A8: W2 .last() in B by A4, A7;

W .first() = a by A6;

then W2 .first() in A by A5, A7;

then len W2 in { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } by A8;

then reconsider X = { (len P) where P is Path of G : ( P .first() in A & P .last() in B ) } as non empty Subset of NAT by A3;

min X in X by XXREAL_2:def 7;

then consider M being Path of G such that

A9: len M = min X and

A10: M .first() in A and

A11: M .last() in B ;

now :: thesis: for P2 being Path of G st P2 is_Walk_from M .first() ,M .last() holds

len P2 >= len M

then A14:
M is minlength
by Th37;len P2 >= len M

let P2 be Path of G; :: thesis: ( P2 is_Walk_from M .first() ,M .last() implies len P2 >= len M )

assume A12: P2 is_Walk_from M .first() ,M .last() ; :: thesis: len P2 >= len M

A13: P2 .last() in B by A11, A12;

P2 .first() in A by A10, A12;

then len P2 in X by A13;

hence len P2 >= len M by A9, XXREAL_2:def 7; :: thesis: verum

end;assume A12: P2 is_Walk_from M .first() ,M .last() ; :: thesis: len P2 >= len M

A13: P2 .last() in B by A11, A12;

P2 .first() in A by A10, A12;

then len P2 in X by A13;

hence len P2 >= len M by A9, XXREAL_2:def 7; :: thesis: verum

A15: now :: thesis: for n being odd Nat st 1 < n & n < len M holds

( not M . n in A & not M . n in B )

M .first() <> M .last()
by A2, A10, A11, XBOOLE_0:def 4;( not M . n in A & not M . n in B )

let n be odd Nat; :: thesis: ( 1 < n & n < len M implies ( not M . n in A & not M . n in B ) )

assume that

A16: 1 < n and

A17: n < len M ; :: thesis: ( not M . n in A & not M . n in B )

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

assume A18: ( M . n in A or M . n in B ) ; :: thesis: contradiction

end;assume that

A16: 1 < n and

A17: n < len M ; :: thesis: ( not M . n in A & not M . n in B )

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

assume A18: ( M . n in A or M . n in B ) ; :: thesis: contradiction

per cases
( M . n in A or M . n in B )
by A18;

end;

suppose A19:
M . n in A
; :: thesis: contradiction

reconsider T = M .cut (nn,(len M)) as Path of G ;

A20: T .last() in B by A11, A17, GLIB_001:37;

(len T) + nn = (len M) + 1 by A17, GLIB_001:36;

then A21: (len T) + 0 < (((len M) + 1) + (- n)) + (n + (- 1)) by A16, XREAL_1:8;

T .first() in A by A17, A19, GLIB_001:37;

then len T in X by A20;

hence contradiction by A9, A21, XXREAL_2:def 7; :: thesis: verum

end;A20: T .last() in B by A11, A17, GLIB_001:37;

(len T) + nn = (len M) + 1 by A17, GLIB_001:36;

then A21: (len T) + 0 < (((len M) + 1) + (- n)) + (n + (- 1)) by A16, XREAL_1:8;

T .first() in A by A17, A19, GLIB_001:37;

then len T in X by A20;

hence contradiction by A9, A21, XXREAL_2:def 7; :: thesis: verum

suppose A22:
M . n in B
; :: thesis: contradiction

reconsider T = M .cut (1,nn) as Path of G ;

A23: (2 * 0) + 1 <= n by A16;

then A24: T .last() = M . nn by A17, GLIB_001:37;

(2 * 0) + 1 <= n by A16;

then A25: (len T) + 1 = nn + 1 by A17, GLIB_001:36;

T .first() = M . 1 by A17, A23, GLIB_001:37;

then len T in X by A10, A22, A24;

hence contradiction by A9, A17, A25, XXREAL_2:def 7; :: thesis: verum

end;A23: (2 * 0) + 1 <= n by A16;

then A24: T .last() = M . nn by A17, GLIB_001:37;

(2 * 0) + 1 <= n by A16;

then A25: (len T) + 1 = nn + 1 by A17, GLIB_001:36;

T .first() = M . 1 by A17, A23, GLIB_001:37;

then len T in X by A10, A22, A24;

hence contradiction by A9, A17, A25, XXREAL_2:def 7; :: thesis: verum

then not M is trivial by GLIB_001:127;

hence ex P being Path of G st

( P is minlength & not P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds

( not P . n in A & not P . n in B ) ) ) by A10, A11, A14, A15; :: thesis: verum