:: deftheorem DefClassical defines classical HILBERT4:def 10 :
for p being Element of HP-WFF holds
( p is classical iff for v being SetValuation0 holds SetVal0 (v,p) <> {} );