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 st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k