theorem Th12: :: HILBERT1:12

for T being Subset of HP-WFF holds
( T is Hilbert_theory iff CnPos T = T )