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