for p being Element of HP-WFF holds (Subformulae p) . {} = p