proposition: Lemma subnet_limit: forall (x0:X) {J:DirectedSet} (y:Net J X), net_limit x x0 -> Subnet x y -> net_limit y x0.
proof: Proof. intros. destruct H0. red. intros. destruct (H U H2 H3). destruct (H1 x1). destruct H5, H6. exists x3. intros. apply H4. apply preord_trans with x2; trivial. - apply DS_ord_cond. - rewrite <- H6. now apply H0. Qed.