ex o being BinOp of REAL st
for a, b being Element of REAL holds o . (a,b) = min (a,b) from BINOP_1:sch 4();
hence ex b₁ being BinOp of REAL st
for x, y being Real holds b₁ . (x,y) = min (x,y) ; :: thesis: verum