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 9;
then consider x being object 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 6;
reconsider f = x as Element of dom (Subformulae q) by A1;
A4: (Subformulae q) | f = Subformulae p by A3, Th35;
A5: not p is conditional
proof
assume p is conditional ; :: thesis: contradiction
then consider r, s being Element of HP-WFF such that
A6: p = r => s ;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A6, Th33;
hence contradiction by A2, A4, TREES_9:6; :: thesis: verum
end;
not p is conjunctive
proof
assume p is conjunctive ; :: thesis: contradiction
then consider r, s being Element of HP-WFF such that
A7: p = r '&' s ;
Subformulae p = p -tree ((Subformulae r),(Subformulae s)) by A7, Th32;
hence contradiction by A2, A4, TREES_9:6; :: thesis: verum
end;
hence ( p = VERUM or p is simple ) by A5, Th9; :: thesis: verum