for m being Element of NAT holds
( {} is_CRS_of m iff m = 0 )