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