for k being Element of NAT holds {} is relation_length of k