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