consider f being BinOp of (OpenClosedSet T) such that

A2: for x, y being Element of OpenClosedSet T holds f . (x,y) = H_{2}(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 A2; :: thesis: verum

A2: 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 A2; :: thesis: verum