:: deftheorem defines VERUM HILBERT1:def 7 :
VERUM = <*0*>;