let G be _Graph; :: thesis: for P being Path of G st P is open & P is chordless holds
for m, n being odd Nat st m < n & n <= len P holds
( ex e being object st e Joins P . m,P . n,G iff m + 2 = n )
let P be Path of G; :: thesis: ( P is open & P is chordless implies for m, n being odd Nat st m < n & n <= len P holds
( ex e being object st e Joins P . m,P . n,G iff m + 2 = n ) )
assume that
A1: P is open and
A2: P is chordless ; :: thesis: for m, n being odd Nat st m < n & n <= len P holds
( ex e being object st e Joins P . m,P . n,G iff m + 2 = n )
A3: P is vertex-distinct by A1, Th32;
let m, n be odd Nat; :: thesis: ( m < n & n <= len P implies ( ex e being object st e Joins P . m,P . n,G iff m + 2 = n ) )
assume that
A4: m < n and
A5: n <= len P ; :: thesis: ( ex e being object st e Joins P . m,P . n,G iff m + 2 = n )
A6: m <= len P by A4, A5, XXREAL_0:2;
A7: m in NAT by ORDINAL1:def 12;
A8: n in NAT by ORDINAL1:def 12;
then A9: P . m <> P . n by A1, A4, A5, A7, GLIB_001:147;

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

assume A10: ex e being object st e Joins P . m,P . n,G ; :: thesis: m + 2 = n

A11: now :: thesis: not m + 2 < n

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

now :: thesis: for f being object st f in P .edges() holds
not f Joins P . m,P . n,G

let f be object ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G )
assume f in P .edges() ; :: thesis: not f Joins P . m,P . n,G
then consider k being odd Element of NAT such that
A13: k < len P and
A14: P . (k + 1) = f by GLIB_001:100;
A15: f Joins P . k,P . (k + 2),G by A13, A14, GLIB_001:def 3;
A16: k + 2 <= len P by A13, Th4;
assume A17: 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 A15, A17;

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

then m = k by A7, A3, A6, A13;
hence contradiction by A5, A8, A3, A12, A16, A18; :: thesis: verum

end;

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

then A20: n = k by A5, A8, A3, A13;
m = k + (2 * 1) by A7, A3, A6, A16, A19;
then A21: m > n by A20, XREAL_1:29;
m + 2 > m by XREAL_1:29;
hence contradiction by A12, A21, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction by A2, A5, A9, A10, A12; :: thesis: verum

end;

m + 2 <= n by A4, Th4;
hence m + 2 = n by A11, XXREAL_0:1; :: thesis: verum

end;

assume A22: m + 2 = n ; :: thesis: ex e being object 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 A4, A5, XXREAL_0:2;
hence P . (m + 1) Joins P . m,P . n,G by A7, A22, GLIB_001:def 3; :: thesis: verum