let G be _Graph; :: thesis: for P being Path of G st not P is closed & not P is chordal holds
for m, n being natural odd number st m < n & n <= len P holds
( ex e being set st e Joins P . m,P . n,G iff m + 2 = n )
let P be Path of G; :: thesis: ( not P is closed & not P is chordal implies for m, n being natural odd number st m < n & n <= len P holds
( ex e being set st e Joins P . m,P . n,G iff m + 2 = n ) )
assume A1: ( not P is closed & not P is chordal ) ; :: thesis: for m, n being natural odd number st m < n & n <= len P holds
( ex e being set st e Joins P . m,P . n,G iff m + 2 = n )
let m, n be odd Nat; :: thesis: ( m < n & n <= len P implies ( ex e being set st e Joins P . m,P . n,G iff m + 2 = n ) )
assume A2: ( m < n & n <= len P ) ; :: thesis: ( ex e being set st e Joins P . m,P . n,G iff m + 2 = n )
A3: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
then A4: P . m <> P . n by A1, A2, GLIB_001:148;
A5: P is vertex-distinct by A1, Th32;
A6: m <= len P by A2, XXREAL_0:2;

hereby :: thesis: ( m + 2 = n implies ex e being set st e Joins P . m,P . n,G )

assume A7: ex e being set st e Joins P . m,P . n,G ; :: thesis: m + 2 = n
A8: m + 2 <= n by A2, Th4;

now

assume A9: m + 2 < n ; :: thesis: contradiction

now

let f be set ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G )
assume A10: f in P .edges() ; :: thesis: not f Joins P . m,P . n,G
consider k being odd Element of NAT such that
A11: ( k < len P & P . (k + 1) = f ) by A10, GLIB_001:101;
A12: k + 2 <= len P by A11, Th4;
A13: f Joins P . k,P . (k + 2),G by A11, GLIB_001:def 3;
assume A14: f Joins P . m,P . n,G ; :: thesis: contradiction

per cases ( ( P . m = P . k & P . n = P . (k + 2) ) or ( P . m = P . (k + 2) & P . n = P . k ) ) by A13, A14, GLIB_000:18;

suppose ( P . m = P . k & P . n = P . (k + 2) ) ; :: thesis: contradiction

then ( m = k & n = k + (2 * 1) ) by A2, A3, A5, A6, A11, A12, GLIB_001:def 29;
hence contradiction by A9; :: thesis: verum

end;

suppose ( P . m = P . (k + 2) & P . n = P . k ) ; :: thesis: contradiction

then ( m = k + (2 * 1) & n = k ) by A2, A3, A5, A6, A11, A12, GLIB_001:def 29;
then A15: m > n by XREAL_1:31;
m + 2 > m by XREAL_1:31;
hence contradiction by A9, A15, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction by A1, A2, A4, A7, A9, Def10; :: thesis: verum

end;

hence m + 2 = n by A8, XXREAL_0:1; :: thesis: verum

end;

assume A16: m + 2 = n ; :: thesis: ex e being set st e Joins P . m,P . n,G
take P . (m + 1) ; :: thesis: P . (m + 1) Joins P . m,P . n,G
m < len P by A2, XXREAL_0:2;
hence P . (m + 1) Joins P . m,P . n,G by A3, A16, GLIB_001:def 3; :: thesis: verum