let p, q be Element of HP-WFF ; :: thesis: Subformulae (p => q) = (p => q) -tree (Subformulae p),(Subformulae q)
consider p', q' being DecoratedTree of such that
A1: ( p' = HP-Subformulae . p & q' = HP-Subformulae . q ) and
HP-Subformulae . (p '&' q) = (p '&' q) -tree p',q' and
A2: HP-Subformulae . (p => q) = (p => q) -tree p',q' by Def9;
thus Subformulae (p => q) = (p => q) -tree (Subformulae p),(Subformulae q) by A1, A2; :: thesis: verum