theorem Th33: :: HILBERT2:33

for p, q being Element of HP-WFF holds Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))