Lemma isaprop_ispartbinophrel {X : setwithbinop} (S : hsubtype X) (R : hrel X) : isaprop (ispartbinophrel S R). Proof. apply isapropdirprod ; apply impred_isaprop ; intros a ; apply impred_isaprop ; intros b ; apply impred_isaprop ; intros c ; apply isapropimpl, isapropimpl, propproperty. Defined.