theorem Th1: :: HILBERT1:1

for X being Subset of HP-WFF holds VERUM in CnPos X