Theorem isisolatedinclb {X Y : UU} (f : X -> Y) (is : isincl f) (x : X) (is0 : isisolated _ (f x)) : isisolated _ x. Proof. intros. unfold isisolated. intro x'. set (a := is0 (f x')). induction a as [ a1 | a2 ]. apply (ii1 (invmaponpathsincl f is _ _ a1)). apply (ii2 ((negf (@maponpaths _ _ f _ _)) a2)). Defined.