theorem :: HILBERT1:13

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