:: deftheorem defines RealFunc_Lattice REAL_LAT:def 6 :
for A being non empty set holds RealFunc_Lattice A = LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);