:: deftheorem defines Real_Lattice REAL_LAT:def 3 :
Real_Lattice = LattStr(# REAL,maxreal,minreal #);