:: deftheorem defines Euclid EUCLID:def 7 :
for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);