theorem Th9: :: HILBERT1:9

for X being Subset of HP-WFF holds X c= CnPos X