let m1, m2 be Element of omega ; :: thesis: ( k divides m1 & n divides m1 & ( for m being natural Ordinal st k divides m & n divides m holds
m1 divides m ) & k divides m2 & n divides m2 & ( for m being natural Ordinal st k divides m & n divides m holds
m2 divides m ) implies m1 = m2 )
assume ( k divides m1 & n divides m1 & ( for m being natural Ordinal st k divides m & n divides m holds
m1 divides m ) & k divides m2 & n divides m2 & ( for m being natural Ordinal st k divides m & n divides m holds
m2 divides m ) ) ; :: thesis: m1 = m2
then ( m1 divides m2 & m2 divides m1 ) ;
hence m1 = m2 by Th8; :: thesis: verum