for p, q being Element of HP-WFF holds p '&' q <> VERUM