let p be Element of HP-WFF ; :: thesis:
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

let x be object ; :: according to TARSKI:def 3 :: thesis:
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:

end;

then reconsider X = { q where q is Element of HP-WFF : q is canonical } as Subset of HP-WFF ;
X is Hilbert_theory

thus VERUM in X ; :: according to HILBERT1:def 10 :: thesis:
let p, q, r be Element of HP-WFF ; :: thesis:
thus p => (q => p) in X ; :: thesis:
thus (p => (q => r)) => ((p => q) => (p => r)) in X ; :: thesis:
thus (p '&' q) => p in X ; :: thesis:
thus (p '&' q) => q in X ; :: thesis:
thus p => (q => (p '&' q)) in X ; :: thesis:
assume p in X ; :: thesis:
then A1: ex s being Element of HP-WFF st
( s = p & s is canonical ) ;
assume p => q in X ; :: thesis:
then ex s being Element of HP-WFF st
( s = p => q & s is canonical ) ;
then q is canonical by A1, Th40;
hence q in X ; :: thesis:

end;

then A2: HP_TAUT c= X by HILBERT1:13;
assume p in HP_TAUT ; :: thesis:
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: