Theorem isapropisisolated (X : UU) (x : X) : isaprop (isisolated X x). Proof. intros. apply isofhlevelsn. intro is. apply impred. intro x'. apply (isapropdec _ (isaproppathsfromisolated X x is x')). Defined.