let i be 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 & 1 < i & i < len dct holds
( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
let Dftn be 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 & 1 < i & i < len dct holds
( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; ( dct . i in places_of dct & 1 < i & i < len dct implies ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i ) )
assume H1:
( dct . i in places_of dct & 1 < i & i < len dct )
; ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
then P1:
i in dom dct
by FINSEQ_3:25;
then H4:
i mod 2 = 1
by Thc, H1;
L1:
[(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn
by The;
L2:
[(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn
by Thd;
consider p being place of Dftn such that
H6:
( p = dct . i & p in rng dct )
by H1;
H8:
1 + 1 <= i
by H1, NAT_1:13;
then reconsider im2 = i - 2 as Element of NAT by NAT_1:21;
then H2:
im2 mod 2 = 1
by NAT_D:12;
P2:
i - 1 < len dct
by H1, XREAL_1:147;
then
[(dct . im2),(dct . (im2 + 1))] in the S-T_Arcs of Dftn
by Def5, H2;
hence
[(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn
; ( [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
[(dct . (im2 + 1)),(dct . (im2 + 2))] in the T-S_Arcs of Dftn
by Def5, H2, P2;
hence
[(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn
; ( [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
H9:
i + 1 <= len dct
by NAT_1:13, H1;
i + 1 <> len dct
then H5:
i + 1 < len dct
by XXREAL_0:1, H9;
hence
[(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn
by Def5, H4; ( [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
thus
[(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn
by Def5, H5, H4; 3 <= i
2 <> i
then
2 < i
by XXREAL_0:1, H8;
then
2 + 1 <= i
by NAT_1:13;
hence
3 <= i
; verum