-(*
-lemma ml_lattice: ∀R.mlattice_ R → lattice.
-intros (R ml); apply (mk_lattice (apart_of_metric_space ? (ml_mspace_ ? ml))); try unfold eq;
-cases (ml_with2_ ? ml);
-[apply (join (ml_lattice_ ? ml));|apply (meet (ml_lattice_ ? ml));
-|apply (join_refl (ml_lattice_ R ml));| apply (meet_refl (ml_lattice_ ? ml));
-|apply (join_comm (ml_lattice_ ? ml));| apply (meet_comm (ml_lattice_ ? ml));
-|apply (join_assoc (ml_lattice_ ? ml));|apply (meet_assoc (ml_lattice_ ? ml));
-|apply (absorbjm (ml_lattice_ ? ml)); |apply (absorbmj (ml_lattice_ ? ml));
-|apply (strong_extj (ml_lattice_ ? ml));|apply (strong_extm (ml_lattice_ ? ml));]
-qed.
-
-coercion cic:/matita/metric_lattice/ml_lattice.con.
-*)
-