:: deftheorem defines EMINFTY SRINGS_5:def 21 :
for n being non zero Nat holds EMINFTY n = MetrStruct(# (REAL n),(Infty_dist n) #);