Lemma isaprop_isTRR (V : hSet) (E : hrel V) (r : V) : isaprop (isTRR V E r). Proof. apply isapropdirprod. - apply (isaprop_isrefl E). - apply isapropdirprod. -- apply (isaprop_istrans E). -- apply (isaprop_isaroot E r). Qed.