:: deftheorem defines x. GRZLOG_1:def 10 :
for n being Element of NAT holds x. n = <*0,n*>;