for p, q being Element of NatPlus_Lattice holds p "/\" q = (@ p) gcd (@ q) ;