let IT1, IT2 be Nat; :: thesis: ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT2 ) implies IT1 = IT2 )
assume ( IT1 divides a & IT1 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT1 ) & IT2 divides a & IT2 divides b & ( for m being Integer st m divides a & m divides b holds
m divides IT2 ) ) ; :: thesis: IT1 = IT2
then ( IT1 divides IT2 & IT2 divides IT1 ) ;
hence IT1 = IT2 by Lm8; :: thesis: verum