consider f being BinOp of (OpenClosedSet T) such that

A1: for x, y being Element of OpenClosedSet T holds f . (x,y) = H_{1}(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

A1: for x, y being Element of OpenClosedSet T holds f . (x,y) = H

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