:: deftheorem defines SUB HEYTING2:def 6 :
for V being set
for C being finite set
for u being Element of (SubstLatt (V,C)) holds SUB u = bool u;