let m, n be natural Ordinal; :: thesis: m lcm n divides m *^ n
( m divides m *^ n & n divides m *^ n ) ;
hence m lcm n divides m *^ n by Def4; :: thesis: verum