:: deftheorem defines x. ZF_LANG:def 2 :
for n being Element of NAT holds x. n = 5 + n;