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 & 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 & 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 & 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 & 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

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;

consider b being object such that
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

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;

then A14: M is minlength by Th37;

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 )

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

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

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;

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;

end;

end;

M .first() <> M .last() by A2, A10, A11, XBOOLE_0:def 4;
then M is trivial by GLIB_001:127;
hence ex P being Path of G st
( P is minlength & 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