let p, q be Element of HP-WFF ; :: thesis: Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))
ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = HP-Subformulae . p & q9 = HP-Subformulae . q & HP-Subformulae . (p '&' q) = (p '&' q) -tree (p9,q9) & HP-Subformulae . (p => q) = (p => q) -tree (p9,q9) ) by Def9;
hence Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q)) ; :: thesis: verum