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 )

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 )

( 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 A3:
for x1, x2 being Element of FT st x1 in A & x2 in A holds
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

end;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;

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;

hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: verum

end;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;

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;

hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; :: thesis: verum

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

hence
A is arcwise_connected
; :: thesis: verum
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;

( g is continuous & rng g c= A ) by A4;

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;( 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;

( g is continuous & rng g c= A ) by A4;

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