for p being Element of HP-WFF st p . 1 = 0 holds
p = VERUM