theorem :: FINTOPO6:58

for FT being non empty RelStr
for g being FinSequence of FT
for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )