let X be Subset of HP-WFF; :: thesis: for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
let p, q be Element of HP-WFF ; :: thesis: (p '&' q) => p in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p '&' q) => p in T ;
hence (p '&' q) => p in CnPos X by Def11; :: thesis: verum