:: deftheorem Def10 defines Hilbert_theory HILBERT1:def 10 :
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) ) );