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;

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

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 A22:
m + 2 = n
; :: thesis: ex e being object st e Joins P . m,P . n,Gassume A10:
ex e being object st e Joins P . m,P . n,G
; :: thesis: m + 2 = n

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

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

m + 2 <= n
by A4, Th4;assume A12:
m + 2 < n
; :: thesis: contradiction

end;now :: thesis: for f being object st f in P .edges() holds

not f Joins P . m,P . n,G

hence
contradiction
by A2, A5, A9, A10, A12; :: thesis: verumnot 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

end;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;

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;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

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

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