theorem Th6: :: ARYTM_3:6

for m, n being natural Ordinal st {} in m holds
n mod^ m in m