:: deftheorem defines Subformulae HILBERT2:def 10 :
for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;