proposition: Lemma net_limit_is_cluster_point: forall (x:Net I X) (x0:X), net_limit x x0 -> net_cluster_point x x0.
proof: Proof. intros. red. intros. red. intros. destruct (H U H0 H1). destruct (DS_join_cond i x1). destruct H3. exists x2. split; trivial. now apply H2. Qed.