:: deftheorem defines - HEYTING2:def 2 :
for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) holds - A = { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } ;