:: deftheorem Def8 defines simple HILBERT2:def 8 :
for p being Element of HP-WFF holds
( p is simple iff ex n being Element of NAT st p = prop n );