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

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