Definition ispartbinophrellogeqf {X : setwithbinop} (S : hsubtype X) {L R : hrel X} (lg : hrellogeq L R) (isl : ispartbinophrel S L) : ispartbinophrel S R. Proof. split. - intros a b c is rab. apply ((pr1 (lg _ _) ((pr1 isl) _ _ _ is (pr2 (lg _ _) rab)))). - intros a b c is rab. apply ((pr1 (lg _ _) ((pr2 isl) _ _ _ is (pr2 (lg _ _) rab)))). Defined.