let G be _Graph; :: thesis: for P being Path of G

for m, n being odd Nat st m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) holds

( m = len P & n = 1 )

let P be Path of G; :: thesis: for m, n being odd Nat st m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) holds

( m = len P & n = 1 )

let m, n be odd Nat; :: thesis: ( m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) implies ( m = len P & n = 1 ) )

assume that

A1: m <= len P and

A2: n <= len P and

A3: P . m = P . n ; :: thesis: ( m = n or ( m = 1 & n = len P ) or ( m = len P & n = 1 ) )

A4: m in NAT by ORDINAL1:def 12;

A5: n in NAT by ORDINAL1:def 12;

( m = n or m < n or n < m ) by XXREAL_0:1;

hence ( m = n or ( m = 1 & n = len P ) or ( m = len P & n = 1 ) ) by A1, A2, A3, A4, A5, GLIB_001:def 28; :: thesis: verum

for m, n being odd Nat st m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) holds

( m = len P & n = 1 )

let P be Path of G; :: thesis: for m, n being odd Nat st m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) holds

( m = len P & n = 1 )

let m, n be odd Nat; :: thesis: ( m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) implies ( m = len P & n = 1 ) )

assume that

A1: m <= len P and

A2: n <= len P and

A3: P . m = P . n ; :: thesis: ( m = n or ( m = 1 & n = len P ) or ( m = len P & n = 1 ) )

A4: m in NAT by ORDINAL1:def 12;

A5: n in NAT by ORDINAL1:def 12;

( m = n or m < n or n < m ) by XXREAL_0:1;

hence ( m = n or ( m = 1 & n = len P ) or ( m = len P & n = 1 ) ) by A1, A2, A3, A4, A5, GLIB_001:def 28; :: thesis: verum