hereby :: thesis: ( not v in W .vertices() implies ex b_{1} being odd Element of NAT st b_{1} = len W )

thus
( not v in W .vertices() implies ex bdefpred S_{1}[ Nat] means ( $1 is odd & $1 <= len W & W . $1 = v );

assume A1: v in W .vertices() ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT ) )

then A2: W . (W .find v) = v by Def19;

W .find v <= len W by A1, Def19;

then A3: ex k being Nat st S_{1}[k]
by A2;

A4: for k being Nat st S_{1}[k] holds

k <= len W ;

consider IT being Nat such that

A5: ( S_{1}[IT] & ( for n being Nat st S_{1}[n] holds

n <= IT ) ) from NAT_1:sch 6(A4, A3);

reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT ) )

thus ( IT <= len W & W . IT = v ) by A5; :: thesis: for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT

let n be odd Element of NAT ; :: thesis: ( n <= len W & W . n = v implies n <= IT )

assume that

A6: n <= len W and

A7: W . n = v ; :: thesis: n <= IT

thus n <= IT by A5, A6, A7; :: thesis: verum

end;assume A1: v in W .vertices() ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT ) )

then A2: W . (W .find v) = v by Def19;

W .find v <= len W by A1, Def19;

then A3: ex k being Nat st S

A4: for k being Nat st S

k <= len W ;

consider IT being Nat such that

A5: ( S

n <= IT ) ) from NAT_1:sch 6(A4, A3);

reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT ) )

thus ( IT <= len W & W . IT = v ) by A5; :: thesis: for n being odd Element of NAT st n <= len W & W . n = v holds

n <= IT

let n be odd Element of NAT ; :: thesis: ( n <= len W & W . n = v implies n <= IT )

assume that

A6: n <= len W and

A7: W . n = v ; :: thesis: n <= IT

thus n <= IT by A5, A6, A7; :: thesis: verum