:: deftheorem defines EuklSpace3 METRIC_3:def 23 :
EuklSpace3 = MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);