proposition: Lemma subnet_cluster_point: forall (x0:X) {J:DirectedSet} (y:Net J X), net_cluster_point y x0 -> Subnet x y -> net_cluster_point x x0.
proof: Proof. intros. destruct H0 as [h h_increasing h_dominant]. red. intros. red. intros. destruct (h_dominant i). destruct H2, H3. destruct (H U H0 H1 x2). destruct H4. exists (h x3). split; trivial. apply preord_trans with x1; trivial. - apply DS_ord_cond. - rewrite <- H3. now apply h_increasing. Qed.