deffunc H₁( Real, Real) -> Element of REAL = In ((max ($1,$2)),REAL);
consider o being BinOp of REAL such that
A4: 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) = max (x,y)
let a, b be Real; :: thesis: o . (a,b) = max (a,b)
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
o . (a,b) = H₁(a,b) by A4;
hence o . (a,b) = max (a,b) ; :: thesis: verum