for m, n being natural Ordinal holds m lcm n divides m *^ n