defpred S₁[ Element of HP-WFF ] means HP-Subformulae . $1 is DecoratedTree of HP-WFF ;
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
HP-Subformulae . (prop n) = root-tree (prop n) by Def9;
hence S₁[ prop n] ; :: thesis: verum

end;

A2: for r, s being Element of HP-WFF st S₁[r] & S₁[s] holds
( S₁[r '&' s] & S₁[r => s] )

proof

let r, s be Element of HP-WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) )
ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = HP-Subformulae . r & q9 = HP-Subformulae . s & HP-Subformulae . (r '&' s) = (r '&' s) -tree (p9,q9) & HP-Subformulae . (r => s) = (r => s) -tree (p9,q9) ) by Def9;
hence ( S₁[r] & S₁[s] implies ( S₁[r '&' s] & S₁[r => s] ) ) ; :: thesis: verum

end;

A3: S₁[ VERUM ] by Def9;
for p being Element of HP-WFF holds S₁[p] from HILBERT2:sch 2(A3, A1, A2);
hence HP-Subformulae . p is DecoratedTree of HP-WFF ; :: thesis: verum