theorem :: HILBERT2:13

for n being Element of NAT
for p being Element of HP-WFF st p . 1 = 3 + n holds
p is simple