:: deftheorem Def5 defines minfuncreal REAL_LAT:def 5 :
for A being non empty set
for b₂ being BinOp of (Funcs (A,REAL)) holds
( b₂ = minfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b₂ . (f,g) = minreal .: (f,g) );