per cases ( k = {} or n = {} or ( k <> {} & n <> {} ) ) ;

suppose A1: ( k = {} or n = {} ) ; :: thesis: ex b₁ being Element of omega st
( b₁ divides k & b₁ divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b₁ ) )

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

end;

suppose A2: ( k <> {} & n <> {} ) ; :: thesis: ex b₁ being Element of omega st
( b₁ divides k & b₁ divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b₁ ) )

reconsider l = (k *^ n) div^ (k lcm n) as Element of omega by ORDINAL1:def 12;
take l ; :: thesis: ( l divides k & l divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides l ) )
thus ( l divides k & l divides n ) by A2, Th13; :: thesis: for m being natural Ordinal st m divides k & m divides n holds
m divides l
let m be natural Ordinal; :: thesis: ( m divides k & m divides n implies m divides l )
assume that
A3: m divides k and
A4: m divides n ; :: thesis: m divides l
A5: n = m *^ (n div^ m) by A4, Th7;
then A6: n div^ m <> {} by A2, ORDINAL2:35;
(m *^ (k div^ m)) *^ (n div^ m) = n *^ (k div^ m) by A5, ORDINAL3:50;
then A7: n divides (m *^ (k div^ m)) *^ (n div^ m) ;
set mm = m *^ ((k div^ m) *^ (n div^ m));
A8: m *^ ((k div^ m) *^ (n div^ m)) = (m *^ (k div^ m)) *^ (n div^ m) by ORDINAL3:50;
A9: k = m *^ (k div^ m) by A3, Th7;
then k div^ m <> {} by A2, ORDINAL2:35;
then A10: (k div^ m) *^ (n div^ m) <> {} by A6, ORDINAL3:31;
k divides (m *^ (k div^ m)) *^ (n div^ m) by A9;
then k lcm n divides (m *^ (k div^ m)) *^ (n div^ m) by A7, Def4;
then A11: m *^ ((k div^ m) *^ (n div^ m)) = (k lcm n) *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n)) by A8, Th7;
m <> {} by A2, A9, ORDINAL2:35;
then k lcm n <> {} by A11, A10, ORDINAL2:35, ORDINAL3:31;
then A12: ( k *^ n = (k *^ n) +^ {} & {} in k lcm n ) by ORDINAL2:27, ORDINAL3:8;
(m *^ ((k div^ m) *^ (n div^ m))) *^ m = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) by A11, ORDINAL3:50;
then k *^ n = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) by A9, A5, A8, ORDINAL3:50;
then l = m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n)) by A12, ORDINAL3:66;
hence m divides l ; :: thesis: verum

end;

end;