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