let IT1, IT2 be odd Element of NAT ; :: thesis: ( ( v in W .vertices() & IT1 <= len W & W . IT1 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT1 ) & IT2 <= len W & W . IT2 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT2 ) 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 v in W .vertices() ; :: thesis: ( IT1 <= len W & W . IT1 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT1 ) & IT2 <= len W & W . IT2 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT2 ) implies IT1 = IT2 )
assume that
A8: IT1 <= len W and
A9: W . IT1 = v and
A10: for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT1 ; :: thesis: ( IT2 <= len W & W . IT2 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT2 ) implies IT1 = IT2 )
assume that
A11: IT2 <= len W and
A12: W . IT2 = v and
A13: for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT2 ; :: thesis: IT1 = IT2
A14: IT1 <= IT2 by A8, A9, A13;
IT2 <= IT1 by A10, A11, A12;
hence IT1 = IT2 by A14, XXREAL_0:1; :: thesis: verum

end;

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