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