let p be Element of HP-WFF ; :: thesis: (Subformulae p) . {} = p

per cases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;

suppose p is conjunctive ; :: thesis: (Subformulae p) . {} = p

then consider r, s being Element of HP-WFF such that
A1: p = r '&' s by Def6;
Subformulae p = p -tree (Subformulae r),(Subformulae s) by A1, Th32;
hence (Subformulae p) . {} = p by Th6; :: thesis: verum

end;

suppose p is conditional ; :: thesis: (Subformulae p) . {} = p

then consider r, s being Element of HP-WFF such that
A2: p = r => s by Def7;
Subformulae p = p -tree (Subformulae r),(Subformulae s) by A2, Th33;
hence (Subformulae p) . {} = p by Th6; :: thesis: verum

end;

suppose p is simple ; :: thesis: (Subformulae p) . {} = p

then consider n being Element of NAT such that
A3: p = prop n by Def8;
Subformulae p = root-tree p by A3, Def9;
hence (Subformulae p) . {} = p by TREES_4:3; :: thesis: verum

end;

suppose p = VERUM ; :: thesis: (Subformulae p) . {} = p

hence (Subformulae p) . {} = p by Th30, TREES_4:3; :: thesis: verum

end;

end;