:: deftheorem defines @' GR_CY_1:def 6 :
for h being Integer holds @' h = h;