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 that
A13: ( a divides IT1 & b divides IT1 ) and
A14: for m being Integer st a divides m & b divides m holds
IT1 divides m and
A15: ( a divides IT2 & b divides IT2 ) and
A16: for m being Integer st a divides m & b divides m holds
IT2 divides m ; :: thesis: IT1 = IT2
( IT1 divides IT2 & IT2 divides IT1 ) by A13, A14, A15, A16;
hence IT1 = IT2 by Lm8; :: thesis: verum