:: deftheorem Def39 defines inf_path MODELC_1:def 39 :
for S being non empty set
for R being total Relation of S,S
for b₃ being sequence of S holds
( b₃ is inf_path of R iff for n being Nat holds [(b₃ . n),(b₃ . (n + 1))] in R );