:: deftheorem defines @ GROUP_4:def 1 :
for i being Integer holds @ i = i;