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