:: deftheorem defines SetVal0 HILBERT4:def 9 :
for v being SetValuation0
for p being Element of HP-WFF holds SetVal0 (v,p) = (SetVal0 v) . p;