let X be Subset of ; :: 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 st T is Hilbert_theory & X c= T holds
p => (q => (p '&' q)) in T by Def10;
hence p => (q => (p '&' q)) in CnPos X by Def11; :: thesis: verum