let p be Element of HP-WFF ; :: thesis: ( p in HP_TAUT implies p is canonical )
set X = { q where q is Element of HP-WFF : q is canonical } ;
{ q where q is Element of HP-WFF : q is canonical } c= HP-WFF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of HP-WFF : q is canonical } or x in HP-WFF )
assume x in { q where q is Element of HP-WFF : q is canonical } ; :: thesis:
then ex p being Element of HP-WFF st
( p = x & p is canonical ) ;
hence x in HP-WFF ; :: thesis: verum
end;
then reconsider X = { q where q is Element of HP-WFF : q is canonical } as Subset of HP-WFF ;
X is Hilbert_theory
proof
thus VERUM in X ; :: according to HILBERT1:def 10 :: thesis: for b1, b2, b3 being Element of HP-WFF holds
( b1 => (b2 => b1) in X & (b1 => (b2 => b3)) => ((b1 => b2) => (b1 => b3)) in X & (b1 '&' b2) => b1 in X & (b1 '&' b2) => b2 in X & b1 => (b2 => (b1 '&' b2)) in X & ( not b1 in X or not b1 => b2 in X or b2 in X ) )

let p, q, r be Element of HP-WFF ; :: thesis: ( p => (q => p) in X & (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )
thus p => (q => p) in X ; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in X ; :: thesis: ( (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )
thus (p '&' q) => p in X ; :: thesis: ( (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )
thus (p '&' q) => q in X ; :: thesis: ( p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )
thus p => (q => (p '&' q)) in X ; :: thesis: ( not p in X or not p => q in X or q in X )
assume p in X ; :: thesis: ( not p => q in X or q in X )
then A1: ex s being Element of HP-WFF st
( s = p & s is canonical ) ;
assume p => q in X ; :: thesis: q in X
then ex s being Element of HP-WFF st
( s = p => q & s is canonical ) ;
then q is canonical by ;
hence q in X ; :: thesis: verum
end;
then A2: HP_TAUT c= X by HILBERT1:13;
assume p in HP_TAUT ; :: thesis: p is canonical
then p in X by A2;
then ex q being Element of HP-WFF st
( p = q & q is canonical ) ;
hence p is canonical ; :: thesis: verum