theorem :: INT_4:48

for m being Element of NAT holds { a where a is Nat : a < m } is_CRS_of m