:: deftheorem defines VAR GRZLOG_1:def 1 :
VAR = { <*0,k*> where k is Element of NAT : verum } ;