Lemma iscomp2binoptransrel {X : setwith2binop} (R : hrel X) (is : istrans R) (isb : is2binophrel R) : (iscomprelrelfun2 R R (@op1 X)) × (iscomprelrelfun2 R R (@op2 X)). Proof. split. - apply (@iscompbinoptransrel (setwithbinop1 X) R is (pr1 isb)). - apply (@iscompbinoptransrel (setwithbinop2 X) R is (pr2 isb)). Defined.