deffunc H₁( Real, Real) -> Element of REAL = In ((min ($1,$2)),REAL);
consider o being BinOp of REAL such that
A1: for a, b being Element of REAL holds o . (a,b) = H₁(a,b) from BINOP_1:sch 4();
take o ; :: thesis: for x, y being Real holds o . (x,y) = min (x,y)
let a, b be Real; :: thesis: o . (a,b) = min (a,b)
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
o . (aa,bb) = H₁(aa,bb) by A1;
hence o . (a,b) = min (a,b) ; :: thesis: verum