theorem :: FINTOPO6:50

for FT being non empty RelStr
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 )