:: deftheorem defines NatPlus_Lattice NAT_LAT:def 10 :
NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #);