per cases ;

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

reconsider w = {} as Element of omega by ORDINAL1:def 13;
take w ; :: thesis:
thus ( k divides w & n divides w ) by Th14; :: thesis:
let m be natural Ordinal; :: thesis:
assume ( k divides m & n divides m ) ; :: thesis:
hence w divides m by A1; :: thesis:

end;

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

A3: ( k divides k *^ n & n divides k *^ n ) by Def3;
defpred S₂[ Ordinal] means ex m being natural Ordinal st
( $1 = m & k divides m & n divides m & k c= m );
{} c= n ;
then {} c< n by A2, XBOOLE_0:def 8;
then {} in n by ORDINAL1:21;
then 1 c= n by Lm3, ORDINAL1:33;
then ( k *^ 1 = k & k *^ 1 c= k *^ n ) by ORDINAL2:56, ORDINAL2:58;
then A4: ex A being Ordinal st S₂[A] by A3;
consider A being Ordinal such that
A5: S₂[A] and
A6: for B being Ordinal st S₂[B] holds
A c= B from ORDINAL1:sch 1(A4);
consider l being natural Ordinal such that
A7: ( A = l & k divides l & n divides l & k c= l ) by A5;
reconsider l = l as Element of omega by ORDINAL1:def 13;
take l ; :: thesis:
thus ( k divides l & n divides l ) by A7; :: thesis:
let m be natural Ordinal; :: thesis:
assume A8: ( k divides m & n divides m ) ; :: thesis:

{} c= k ;
then {} c< k by A2, XBOOLE_0:def 8;
then A9: {} in k by ORDINAL1:21;
A10: m = (l *^ (m div^ l)) +^ (m mod^ l) by ORDINAL3:78;
( l = k *^ (l div^ k) & l = n *^ (l div^ n) ) by A7, Th11;
then ( l *^ (m div^ l) = k *^ ((l div^ k) *^ (m div^ l)) & l *^ (m div^ l) = n *^ ((l div^ n) *^ (m div^ l)) ) by ORDINAL3:58;
then ( k divides l *^ (m div^ l) & n divides l *^ (m div^ l) ) by Def3;
then A11: ( k divides m mod^ l & n divides m mod^ l ) by A8, A10, Th16;

assume A12: m mod^ l <> {} ; :: thesis:
{} c= m mod^ l ;
then {} c< m mod^ l by A12, XBOOLE_0:def 8;
then k c= m mod^ l by A11, Th15, ORDINAL1:21;
then l c= m mod^ l by A6, A7, A11;
hence contradiction by A7, A9, Th10, ORDINAL1:7; :: thesis:

end;

then m = l *^ (m div^ l) by A10, ORDINAL2:44;
hence l divides m by Th11; :: thesis:

end;

hence l divides m ; :: thesis:

end;