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