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