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