:: deftheorem defines SetVal HILBERT3:def 3 :
for V being SetValuation
for p being Element of HP-WFF holds SetVal (V,p) = (SetVal V) . p;