proposition: Lemma net_cluster_point_impl_subnet_converges: exists J:DirectedSet, exists y:Net J X, Subnet x y /\ net_limit y x0.
proof: Proof. exists cluster_point_subnet_DS. exists cluster_point_subnet. split. - exact cluster_point_subnet_is_subnet. - exact cluster_point_subnet_converges. Qed.