let FT be non empty RelStr ; :: thesis: for A being Subset of FT

for x1, x2 being Element of FT st ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds

ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds

ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

let x1, x2 be Element of FT; :: thesis: ( ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )

given f being FinSequence of FT such that A1: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; :: thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

consider g2 being FinSequence of FT such that

A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g2 <= len h ) ) by A1, Lm4;

g2 is_minimum_path_in A,x1,x2 by A2;

hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: verum

for x1, x2 being Element of FT st ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds

ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds

ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

let x1, x2 be Element of FT; :: thesis: ( ex f being FinSequence of FT st

( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )

given f being FinSequence of FT such that A1: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; :: thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2

consider g2 being FinSequence of FT such that

A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g2 <= len h ) ) by A1, Lm4;

g2 is_minimum_path_in A,x1,x2 by A2;

hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: verum