let k, l be Element of NAT ; :: thesis: ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) implies k = l )
assume ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) ) ; :: thesis: k = l
then ( k <= l & l <= k ) ;
hence k = l by XXREAL_0:1; :: thesis: verum