theorem :: INT_2:20

for a, b being Integer holds a gcd b is Element of NAT by ORDINAL1:def 12;