theorem :: INT_8:25

for m being Nat holds
( {} is_RRS_of m iff m = 0 )