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