proposition: Lemma net_cluster_point_in_closure: forall (S:Ensemble X) (x:Net I X) (x0:X), (for large i:DS_set I, In S (x i)) -> net_cluster_point x x0 -> In (closure S) x0.
proof: Proof. intros. apply NNPP. intro. pose proof (H0 (Complement (closure S))). match type of H2 with | ?A -> ?B -> ?C => assert (C) end. { apply H2; trivial. apply closure_closed. } destruct H, (H3 x1), H4. contradiction H5. apply closure_inflationary. now apply H. Qed.