:: deftheorem defines SUB HEYTING1:def 10 :
for A being set
for u being Element of (NormForm A) holds SUB u = bool u;