:: deftheorem defines Nat_Lattice NAT_LAT:def 3 :
Nat_Lattice = LattStr(# NAT,lcmlat,hcflat #);