let p, q be Element of HP-WFF ; :: thesis: ( not p in Leaves (Subformulae q) or p = VERUM or p is simple )
assume p in Leaves (Subformulae q) ; :: thesis: ( p = VERUM or p is simple )
then p in (Subformulae q) .: (Leaves (dom (Subformulae q))) by TREES_2:def 10;
then consider x being set such that
A1: x in dom (Subformulae q) and
A2: x in Leaves (dom (Subformulae q)) and
A3: p = (Subformulae q) . x by FUNCT_1:def 12;
reconsider f = x as Element of dom (Subformulae q) by A1;
A4: (Subformulae q) | f = Subformulae p by A3, Th35;
A5: not p is conjunctive

proof

assume p is conjunctive ; :: thesis: contradiction
then consider r, s being Element of HP-WFF such that
A6: p = r '&' s by Def6;
Subformulae p = p -tree (Subformulae r),(Subformulae s) by A6, Th32;
hence contradiction by A2, A4, TREES_9:6; :: thesis: verum

end;

not p is conditional

proof

assume p is conditional ; :: thesis: contradiction
then consider r, s being Element of HP-WFF such that
A7: p = r => s by Def7;
Subformulae p = p -tree (Subformulae r),(Subformulae s) by A7, Th33;
hence contradiction by A2, A4, TREES_9:6; :: thesis: verum

end;

hence ( p = VERUM or p is simple ) by A5, Th9; :: thesis: verum