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

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

hence
W . m <> W . n
; :: thesis: verumassume 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;then A5: n = len W by A2, A3, Def28;

m = 1 by A2, A3, A4, Def28;

hence contradiction by A1, A4, A5; :: thesis: verum