:: deftheorem defines RealSpaceCart3 METRIC_3:def 21 :
RealSpaceCart3 = MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);