for T being Subset of HP-WFF st T is Hilbert_theory holds
HP_TAUT c= T