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 Def6, FINSEQ_1:40; :: thesis: verum