theorem Th5: :: ARYTM_3:5

for a, b being natural Ordinal holds
( a divides b iff ex c being natural Ordinal st b = a *^ c )