consider f being BinOp of (OpenClosedSet T) such that
A1: for x, y being Element of OpenClosedSet T holds f . x,y = H₁(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for A, B being Element of OpenClosedSet T holds f . A,B = A \/ B
let x, y be Element of OpenClosedSet T; :: thesis: f . x,y = x \/ y
thus f . x,y = x \/ y by A1; :: thesis: verum