:: deftheorem defines @ SRINGS_5:def 4 :
for n being Nat
for q being Element of RAT n holds @ q = q;