thus for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = H₂(A,B) ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = H₂(A,B) ) holds
b1 = b2 from BINOP_2:sch 2(); :: thesis: verum