:: deftheorem defines prop HILBERT2:def 1 :
for n being Element of NAT holds prop n = <*(3 + n)*>;