:: deftheorem defines @ SRINGS_5:def 23 :
for n being non zero Nat
for p being Element of (EMINFTY n) holds @ p = p;