let p be Element of HP-WFF ; :: thesis: ( p is conjunctive or p is conditional or p is simple or p = VERUM )
defpred S₁[ Element of HP-WFF ] means ( $1 is conjunctive or $1 is conditional or $1 is simple or $1 = VERUM );
A1: S₁[ VERUM ] ;
A2: for n being Element of NAT holds S₁[ prop n] by Def8;
A3: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] ) by Def6, Def7;
for p being Element of HP-WFF holds S₁[p] from HILBERT2:sch 2(A1, A2, A3);
hence ( p is conjunctive or p is conditional or p is simple or p = VERUM ) ; :: thesis: verum