proposition: Lemma isaprop_ispartbinophrel {X : setwithbinop} (S : hsubtype X) (R : hrel X) : isaprop (ispartbinophrel S R).
proof: Proof. apply isapropdirprod ; apply impred_isaprop ; intros a ; apply impred_isaprop ; intros b ; apply impred_isaprop ; intros c ; apply isapropimpl, isapropimpl, propproperty. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions