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