let IT1, IT2 be odd Element of NAT ; :: thesis: ( ( v in W .vertices() & IT1 <= len W & W . IT1 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT1 <= n ) & IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 ) & ( not v in W .vertices() & IT1 = len W & IT2 = len W implies IT1 = IT2 ) )

thus ( not IT1 = len W or not IT2 = len W or IT1 = IT2 ) ; :: thesis: verum

IT1 <= n ) & IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 ) & ( not v in W .vertices() & IT1 = len W & IT2 = len W implies IT1 = IT2 ) )

hereby :: thesis: ( not v in W .vertices() & IT1 = len W & IT2 = len W implies IT1 = IT2 )

assume
not v in W .vertices()
; :: thesis: ( not IT1 = len W or not IT2 = len W or IT1 = IT2 )assume
v in W .vertices()
; :: thesis: ( IT1 <= len W & W . IT1 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT1 <= n ) & IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 )

assume that

A10: IT1 <= len W and

A11: W . IT1 = v and

A12: for n being odd Nat st n <= len W & W . n = v holds

IT1 <= n ; :: thesis: ( IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 )

assume that

A13: IT2 <= len W and

A14: W . IT2 = v and

A15: for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ; :: thesis: IT1 = IT2

A16: IT2 <= IT1 by A10, A11, A15;

IT1 <= IT2 by A12, A13, A14;

hence IT1 = IT2 by A16, XXREAL_0:1; :: thesis: verum

end;IT1 <= n ) & IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 )

assume that

A10: IT1 <= len W and

A11: W . IT1 = v and

A12: for n being odd Nat st n <= len W & W . n = v holds

IT1 <= n ; :: thesis: ( IT2 <= len W & W . IT2 = v & ( for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ) implies IT1 = IT2 )

assume that

A13: IT2 <= len W and

A14: W . IT2 = v and

A15: for n being odd Nat st n <= len W & W . n = v holds

IT2 <= n ; :: thesis: IT1 = IT2

A16: IT2 <= IT1 by A10, A11, A15;

IT1 <= IT2 by A12, A13, A14;

hence IT1 = IT2 by A16, XXREAL_0:1; :: thesis: verum

thus ( not IT1 = len W or not IT2 = len W or IT1 = IT2 ) ; :: thesis: verum