theorem Th51: :: FINTOPO6:52

for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )