Definition isbinoptoispartbinop {X : setwithbinop} (S : hsubtype X) (L : hrel X) (d2 : isbinophrel L) : ispartbinophrel S L. Proof. unfold isbinophrel in d2. unfold ispartbinophrel. split. - intros a b c is. apply (pr1 d2 a b c). - intros a b c is. apply (pr2 d2 a b c). Defined.