theorem :: HILBERT1:11

for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X