:: deftheorem defines @ HEYTING1:def 3 :
for A being set
for u being Element of (NormForm A) holds @ u = u;