let Dftn be With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn
len dct >= 3 by Def5;
then reconsider ln2 = (len dct) - 2 as Element of NAT by NAT_1:21, XXREAL_0:2;
F8: 1 = (ln2 + 2) mod 2 by Def5
.= ((ln2 mod 2) + (2 mod 2)) mod 2 by NAT_D:66
.= ((ln2 mod 2) + 0) mod 2 by NAT_D:25
.= ln2 mod 2 by NAT_D:65 ;
(len dct) + (- 1) < len dct by XREAL_1:30;
then [(dct . (ln2 + 1)),(dct . (ln2 + 2))] in the T-S_Arcs of Dftn by Def5, F8;
hence [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn ; :: thesis: verum