let X be Subset of HP-WFF; :: thesis: VERUM in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
VERUM in T ;
hence VERUM in CnPos X by Def11; :: thesis: verum