let FT be non empty RelStr ; :: thesis: for x being Element of FT holds {x} is arcwise_connected
let x be Element of FT; :: thesis: {x} is arcwise_connected
set A = {x};
A1: rng <*x*> c= {x} by FINSEQ_1:39;
A2: <*x*> . 1 = x ;
then A3: <*x*> . (len <*x*>) = x by FINSEQ_1:40;
for x1, x2 being Element of FT st x1 in {x} & x2 in {x} holds
ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )

proof

let x1, x2 be Element of FT; :: thesis: ( x1 in {x} & x2 in {x} implies ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) )
assume ( x1 in {x} & x2 in {x} ) ; :: thesis: ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )
then ( x1 = x & x2 = x ) by TARSKI:def 1;
hence ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) by A2, A3, A1; :: thesis: verum

end;

hence {x} is arcwise_connected ; :: thesis: verum