defpred S₁[ Nat] means $1 is_at_least_length_of p;
A1: ex m being Nat st S₁[m] by Lm1;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[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