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 ;
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 ;
A7: m in NAT by ORDINAL1:def 12;
A8: n in NAT by ORDINAL1:def 12;
then A9: P . m <> P . n by ;
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 ;
A16: k + 2 <= len P by ;
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 ;
suppose A18: ( P . m = P . k & P . n = P . (k + 2) ) ; :: thesis: contradiction
end;
suppose A19: ( P . m = P . (k + 2) & P . n = P . k ) ; :: thesis: contradiction
end;
end;
end;
hence contradiction by A2, A5, A9, A10, A12; :: thesis: verum
end;
m + 2 <= n by ;
hence m + 2 = n by ; :: 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 ;
hence P . (m + 1) Joins P . m,P . n,G by ; :: thesis: verum