theorem Th9: :: HILBERT2:9

for p being Element of HP-WFF holds
( p is conjunctive or p is conditional or p is simple or p = VERUM )