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 x in A ; :: thesis: <*x*> is_minimum_path_in A,x,x
then A1: {x} c= A by ZFMISC_1:37;
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 ) )
thus rng <*x*> c= A by A1, FINSEQ_1:55; :: 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:57;
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 Def6, FINSEQ_1:57; :: thesis: verum