per cases ;

suppose A1: ( k = {} or n = {} ) ; :: thesis:

then reconsider m = k \/ n as Element of omega by ORDINAL1:def 13;
take m ; :: thesis:
thus ( m divides k & m divides n ) by A1, Th14; :: thesis:
thus for m being natural Ordinal st m divides k & m divides n holds
m divides m by A1; :: thesis:

end;

suppose A2: ( k <> {} & n <> {} ) ; :: thesis:

reconsider l = (k *^ n) div^ (k lcm n) as Element of omega by ORDINAL1:def 13;
take l ; :: thesis:
thus ( l divides k & l divides n ) by A2, Th18; :: thesis:
let m be natural Ordinal; :: thesis:
set mm = m *^ ((k div^ m) *^ (n div^ m));
assume ( m divides k & m divides n ) ; :: thesis:
then A3: ( k = m *^ (k div^ m) & n = m *^ (n div^ m) ) by Th11;
then (m *^ (k div^ m)) *^ (n div^ m) = n *^ (k div^ m) by ORDINAL3:58;
then ( k divides (m *^ (k div^ m)) *^ (n div^ m) & n divides (m *^ (k div^ m)) *^ (n div^ m) ) by A3, Def3;
then A4: ( k lcm n divides (m *^ (k div^ m)) *^ (n div^ m) & m *^ ((k div^ m) *^ (n div^ m)) = (m *^ (k div^ m)) *^ (n div^ m) ) by Def4, ORDINAL3:58;
then A5: m *^ ((k div^ m) *^ (n div^ m)) = (k lcm n) *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n)) by Th11;
then A6: (m *^ ((k div^ m) *^ (n div^ m))) *^ m = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) by ORDINAL3:58;
A7: ( m <> {} & k div^ m <> {} & n div^ m <> {} ) by A2, A3, ORDINAL2:52;
then (k div^ m) *^ (n div^ m) <> {} by ORDINAL3:34;
then k lcm n <> {} by A5, A7, ORDINAL2:52, ORDINAL3:34;
then ( k *^ n = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) & k *^ n = (k *^ n) +^ {} & {} in k lcm n ) by A3, A4, A6, ORDINAL2:44, ORDINAL3:10, ORDINAL3:58;
then l = m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n)) by ORDINAL3:79;
hence m divides l by Def3; :: thesis:

end;