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