let G be _Graph; :: thesis: for W being Path of G st not W is closed 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: ( not W is closed implies for m, n being odd Element of NAT st m < n & n <= len W holds
W . m <> W . n )
assume A1: not W is closed ; :: 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 A2: ( m < n & n <= len W ) ; :: thesis: W . m <> W . n

now

assume A3: W . m = W . n ; :: thesis: contradiction
then ( m = 1 & n = len W ) by A2, Def28;
hence contradiction by A1, A3, Th119; :: thesis: verum

end;

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