:: deftheorem defines RealSpace METRIC_1:def 13 :
RealSpace = MetrStruct(# REAL,real_dist #);