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