:: deftheorem Def5 defines hcf ARYTM_3:def 5 :
for k, n being natural Ordinal
for b₃ being Element of omega holds
( b₃ = k hcf n iff ( b₃ divides k & b₃ divides n & ( for m being natural Ordinal st m divides k & m divides n holds
m divides b₃ ) ) );