defpred S_{1}[ Nat] means $1 is_at_least_length_of p;

A1: ex m being Nat st S_{1}[m]
by Lm1;

ex k being Nat st

( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A1);

then consider k being Nat such that

A2: ( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds

k <= n ) ) ;

take k ; :: thesis: ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

k <= m ) )

thus ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

k <= m ) ) by A2, ORDINAL1:def 12; :: thesis: verum

A1: ex m being Nat st S

ex k being Nat st

( S

k <= n ) ) from NAT_1:sch 5(A1);

then consider k being Nat such that

A2: ( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds

k <= n ) ) ;

take k ; :: thesis: ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

k <= m ) )

thus ( k is Element of NAT & k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds

k <= m ) ) by A2, ORDINAL1:def 12; :: thesis: verum