for n, k, l being Element of NAT holds min* {n,k,l} = min (n,(min (k,l)))