let T be _Tree; :: thesis: for P being Path of T

for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

let P be Path of T; :: thesis: for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

let i, j be odd Nat; :: thesis: ( i < j & j <= len P implies P . i <> P . j )

assume that

A1: i < j and

A2: j <= len P and

A3: P . i = P . j ; :: thesis: contradiction

reconsider i = i, j = j as odd Element of NAT by ORDINAL1:def 12;

A4: i < j by A1;

then A5: i = 1 by A2, A3, GLIB_001:def 28;

then A6: P is V5() by A1, A2, GLIB_001:126;

P .first() = P .last() by A2, A3, A4, A5, GLIB_001:def 28;

hence contradiction by A6, GLIB_001:def 24; :: thesis: verum

for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

let P be Path of T; :: thesis: for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

let i, j be odd Nat; :: thesis: ( i < j & j <= len P implies P . i <> P . j )

assume that

A1: i < j and

A2: j <= len P and

A3: P . i = P . j ; :: thesis: contradiction

reconsider i = i, j = j as odd Element of NAT by ORDINAL1:def 12;

A4: i < j by A1;

then A5: i = 1 by A2, A3, GLIB_001:def 28;

then A6: P is V5() by A1, A2, GLIB_001:126;

P .first() = P .last() by A2, A3, A4, A5, GLIB_001:def 28;

hence contradiction by A6, GLIB_001:def 24; :: thesis: verum