let FT be non empty RelStr ; :: thesis: for A being Subset of
for x1, x2 being Element of st ex f being FinSequence of st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds
ex g being FinSequence of st g is_minimum_path_in A,x1,x2
let A be Subset of ; :: thesis: for x1, x2 being Element of st ex f being FinSequence of st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds
ex g being FinSequence of st g is_minimum_path_in A,x1,x2
let x1, x2 be Element of ; :: thesis: ( ex f being FinSequence of st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) implies ex g being FinSequence of st g is_minimum_path_in A,x1,x2 )
given f being FinSequence of such that A1: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; :: thesis: ex g being FinSequence of st g is_minimum_path_in A,x1,x2
consider g2 being FinSequence of such that
A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of 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, Def8;
hence ex g being FinSequence of st g is_minimum_path_in A,x1,x2 ; :: thesis: verum