let G be _Graph; :: thesis: for W being Path of G st W is open holds
for m, n being odd Element of NAT st m < n & n <= len W holds
W . m <> W . n
let W be Path of G; :: thesis: ( W is open implies for m, n being odd Element of NAT st m < n & n <= len W holds
W . m <> W . n )
assume A1: W is open ; :: thesis: for m, n being odd Element of NAT st m < n & n <= len W holds
W . m <> W . n
let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W implies W . m <> W . n )
assume that
A2: m < n and
A3: n <= len W ; :: thesis: W . m <> W . n

now :: thesis: not W . m = W . n

assume A4: W . m = W . n ; :: thesis: contradiction
then A5: n = len W by A2, A3, Def28;
m = 1 by A2, A3, A4, Def28;
hence contradiction by A1, A4, A5; :: thesis: verum

end;

hence W . m <> W . n ; :: thesis: verum