proposition: Lemma cluster_point_subnet_is_subnet: Subnet x cluster_point_subnet.
proof: Proof. constructor. - intros. destruct j1, j2. simpl in H. simpl. red in H. tauto. - red. intros. exists i. split. + apply preord_refl, DS_ord_cond. + assert (open_neighborhood Full_set x0). { repeat constructor. apply open_full. } assert (In Full_set (x i)) by constructor. now exists (Build_cluster_point_subnet_DS_set i Full_set H H0). Qed.