let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds
( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
let A be Subset of FT; :: thesis: ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
thus ( A is arcwise_connected implies for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) :: thesis: ( ( for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) implies A is arcwise_connected )

proof

assume A1: A is arcwise_connected ; :: thesis: for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
thus for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 :: thesis: verum

proof

let x1, x2 be Element of FT; :: thesis: ( x1 in A & x2 in A implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
assume ( x1 in A & x2 in A ) ; :: thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
then ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A1, Def7;
then consider g2 being FinSequence of FT such that
A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g2 <= len h ) ) by Lm4;
g2 is_minimum_path_in A,x1,x2 by A2, Def8;
hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: verum

end;

end;

assume A3: for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: A is arcwise_connected
for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 )

proof

let x1, x2 be Element of FT; :: thesis: ( x1 in A & x2 in A implies ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) )
assume ( x1 in A & x2 in A ) ; :: thesis: ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 )
then consider g being FinSequence of FT such that
A4: g is_minimum_path_in A,x1,x2 by A3;
A5: ( g . 1 = x1 & g . (len g) = x2 ) by A4, Def8;
( g is continuous & rng g c= A ) by A4, Def8;
hence ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A5; :: thesis: verum

end;

hence A is arcwise_connected by Def7; :: thesis: verum