theorem Th24: :: HILBERT2:24

for n being Element of NAT
for p, q being Element of HP-WFF holds p '&' q <> prop n