theorem Th8: :: HILBERT1:8

for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
CnPos X c= T by Def11;