theorem :: NAT_LAT:14

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