theorem :: NAT_LAT:2

for p, q being Element of Nat_Lattice holds p "/\" q = p gcd q ;