:: deftheorem Def1 defines object2RAT SRINGS_5:def 5 :
for n being Nat
for q being object st q in RAT n holds
object2RAT (q,n) = q;