:: deftheorem defines VAR ZF_LANG:def 1 :
VAR = { k where k is Element of NAT : 5 <= k } ;