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

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

reconsider w = {} as Element of omega by ORDINAL1:def 12;
take w ; :: thesis: ( k divides w & n divides w & ( for m being natural Ordinal st k divides m & n divides m holds
w divides m ) )
thus ( k divides w & n divides w ) by Th9; :: thesis: for m being natural Ordinal st k divides m & n divides m holds
w divides m
let m be natural Ordinal; :: thesis: ( k divides m & n divides m implies w divides m )
assume ( k divides m & n divides m ) ; :: thesis: w divides m
hence w divides m by A1; :: thesis: verum

end;

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

{} c= k ;
then {} c< k by A2, XBOOLE_0:def 8;
then A3: {} in k by ORDINAL1:11;
{} c= n ;
then {} c< n by A2, XBOOLE_0:def 8;
then {} in n by ORDINAL1:11;
then A4: 1 c= n by Lm3, ORDINAL1:21;
defpred S₂[ Ordinal] means ex m being natural Ordinal st
( $1 = m & k divides m & n divides m & k c= m );
A5: k *^ 1 = k by ORDINAL2:39;
( k divides k *^ n & n divides k *^ n ) ;
then A6: ex A being Ordinal st S₂[A] by A4, A5, ORDINAL2:41;
consider A being Ordinal such that
A7: S₂[A] and
A8: for B being Ordinal st S₂[B] holds
A c= B from ORDINAL1:sch 1(A6);
consider l being natural Ordinal such that
A9: A = l and
A10: k divides l and
A11: n divides l and
A12: k c= l by A7;
reconsider l = l as Element of omega by ORDINAL1:def 12;
take l ; :: thesis: ( k divides l & n divides l & ( for m being natural Ordinal st k divides m & n divides m holds
l divides m ) )
thus ( k divides l & n divides l ) by A10, A11; :: thesis: for m being natural Ordinal st k divides m & n divides m holds
l divides m
let m be natural Ordinal; :: thesis: ( k divides m & n divides m implies l divides m )
assume that
A13: k divides m and
A14: n divides m ; :: thesis: l divides m
A15: m = (l *^ (m div^ l)) +^ (m mod^ l) by ORDINAL3:65;
l = k *^ (l div^ k) by A10, Th7;
then l *^ (m div^ l) = k *^ ((l div^ k) *^ (m div^ l)) by ORDINAL3:50;
then k divides l *^ (m div^ l) ;
then A16: k divides m mod^ l by A13, A15, Th11;
l = n *^ (l div^ n) by A11, Th7;
then l *^ (m div^ l) = n *^ ((l div^ n) *^ (m div^ l)) by ORDINAL3:50;
then n divides l *^ (m div^ l) ;
then A17: n divides m mod^ l by A14, A15, Th11;

now :: thesis: not m mod^ l <> {}

A18: {} c= m mod^ l ;
assume m mod^ l <> {} ; :: thesis: contradiction
then {} c< m mod^ l by A18, XBOOLE_0:def 8;
then k c= m mod^ l by A16, Th10, ORDINAL1:11;
then l c= m mod^ l by A8, A9, A16, A17;
hence contradiction by A12, A3, Th6, ORDINAL1:5; :: thesis: verum

end;

then m = l *^ (m div^ l) by A15, ORDINAL2:27;
hence l divides m ; :: thesis: verum

end;

end;