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