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