theorem :: HILBERT2:14

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