let X be Subset of HP-WFF; :: thesis: CnPos X is Hilbert_theory
thus VERUM in CnPos X by Th1; :: according to HILBERT1:def 10 :: thesis: for p, q, r being Element of HP-WFF holds
( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
let p, q, r be Element of HP-WFF ; :: thesis: ( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus p => (q => p) in CnPos X by Th4; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Th3; :: thesis: ( (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p '&' q) => p in CnPos X by Th5; :: thesis: ( (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p '&' q) => q in CnPos X by Th6; :: thesis: ( p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus p => (q => (p '&' q)) in CnPos X by Th2; :: thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X )
thus ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) by Th7; :: thesis: verum