theorem Th12: :: HILBERT2:12

for p being Element of HP-WFF st p . 1 = 2 holds
p is conjunctive