Definition cutonweq {T : UU} t (is : isisolated T t) (w : T ≃ T) : isolated T × (compl T t ≃ compl T t). Proof. intros. split. - exists (w t). apply isisolatedweqf. assumption. - intermediate_weq (compl T (w t)). + apply weqoncompl. + apply weqtranspos0. * apply isisolatedweqf. assumption. * assumption. Defined.