:: deftheorem defines EuklSpace2 METRIC_3:def 19 :
EuklSpace2 = MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);