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