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