let T be Subset of HP-WFF; :: thesis: ( T is Hilbert_theory implies HP_TAUT c= T )
assume A1: T is Hilbert_theory ; :: thesis: HP_TAUT c= T
HP_TAUT c= CnPos T by Th10, XBOOLE_1:2;
hence HP_TAUT c= T by A1, Th12; :: thesis: verum