}.
notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
-interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b).
+interpretation "metric" 'delta2 a b = (metric ? ? a b).
notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
+interpretation "metric" 'delta = (metric ? ?).
lemma apart_of_metric_space: ∀R.metric_space R → apartness.
intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;