let i be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( [(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;

now :: thesis: not im2 mod 2 = 0

assume im2 mod 2 = 0 ; :: thesis: contradiction
then (im2 + 1) mod 2 = 1 mod 2 by NAT_D:17
.= 2 - 1 by NAT_D:14 ;
then ((im2 + 1) + 1) mod 2 = 0 by NAT_D:69;
hence contradiction by Thc, H1, P1; :: thesis: verum

end;

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 ; :: thesis: ( [(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 ; :: thesis: ( [(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

proof

assume i + 1 = len dct ; :: thesis: contradiction
then dct . ((i + 1) - 1) in the carrier' of Dftn by L1, ZFMISC_1:87;
hence contradiction by NET_1:def 2, XBOOLE_0:3, H6; :: thesis: verum

end;

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; :: thesis: ( [(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; :: thesis: 3 <= i
2 <> i

proof

assume i = 2 ; :: thesis: contradiction
then dct . i in the carrier' of Dftn by L2, ZFMISC_1:87;
hence contradiction by NET_1:def 2, H6, XBOOLE_0:3; :: thesis: verum

end;

then 2 < i by XXREAL_0:1, H8;
then 2 + 1 <= i by NAT_1:13;
hence 3 <= i ; :: thesis: verum