theorem Th34: :: HILBERT2:34

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