:: deftheorem Def13 defines path LTLAXIO4:def 13 :
for P being consistent PNPair
for T being pnptree of P
for b₃ being sequence of (dom T) holds
( b₃ is path of T iff ( b₃ . 0 = {} & ( for k being Nat holds b₃ . (k + 1) in succ (b₃ . k) ) ) );