consider f being BinOp of (OpenClosedSet T) such that
A2: 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 A2; :: thesis: verum