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