proposition: Lemma cluster_point_subnet_converges: net_limit cluster_point_subnet x0.
proof: Proof. red. intros. destruct I_nonempty as [i0]. destruct (x0_cluster_point U H H0 i0). destruct H1. assert (open_neighborhood U x0) by now split. exists (Build_cluster_point_subnet_DS_set x1 U H3 H2). intros. destruct j. red in H4. simpl in H4. red in H4. simpl in H4. unfold cluster_point_subnet. simpl. destruct H4. auto with sets. Qed.