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

for x being Element of FT st x in A holds

<*x*> is_minimum_path_in A,x,x

let A be Subset of FT; :: thesis: for x being Element of FT st x in A holds

<*x*> is_minimum_path_in A,x,x

let x be Element of FT; :: thesis: ( x in A implies <*x*> is_minimum_path_in A,x,x )

assume A1: x in A ; :: thesis: <*x*> is_minimum_path_in A,x,x

thus <*x*> is continuous ; :: according to FINTOPO6:def 8 :: thesis: ( rng <*x*> c= A & <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) )

{x} c= A by A1, ZFMISC_1:31;

hence rng <*x*> c= A by FINSEQ_1:38; :: thesis: ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) )

len <*x*> = 1 by FINSEQ_1:40;

hence ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) ) by FINSEQ_1:40; :: thesis: verum

for x being Element of FT st x in A holds

<*x*> is_minimum_path_in A,x,x

let A be Subset of FT; :: thesis: for x being Element of FT st x in A holds

<*x*> is_minimum_path_in A,x,x

let x be Element of FT; :: thesis: ( x in A implies <*x*> is_minimum_path_in A,x,x )

assume A1: x in A ; :: thesis: <*x*> is_minimum_path_in A,x,x

thus <*x*> is continuous ; :: according to FINTOPO6:def 8 :: thesis: ( rng <*x*> c= A & <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) )

{x} c= A by A1, ZFMISC_1:31;

hence rng <*x*> c= A by FINSEQ_1:38; :: thesis: ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) )

len <*x*> = 1 by FINSEQ_1:40;

hence ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds

len <*x*> <= len h ) ) by FINSEQ_1:40; :: thesis: verum