:: deftheorem Def1 defines minreal REAL_LAT:def 1 :
for b₁ being BinOp of REAL holds
( b₁ = minreal iff for x, y being Real holds b₁ . (x,y) = min (x,y) );