theorem Thc: :: PETRI_DF:7

for i being Nat
for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & i in dom dct holds
i mod 2 = 1