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 13;
i < j by A1;
then A4: ( i = 1 & j = len P ) by A2, A3, GLIB_001:def 28;
then A5: not P is trivial by A1, GLIB_001:127;
P .first() = P .last() by A3, A4;
then P is closed by GLIB_001:def 24;
hence contradiction by A5; :: thesis: verum