let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
let F be Element of QC-WFF A; :: thesis: for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( (tree_of_subformulae F) . t = F iff t = {} )

now :: thesis: ( (tree_of_subformulae F) . t = F implies not t <> {} )

reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22;
assume A1: (tree_of_subformulae F) . t = F ; :: thesis: not t <> {}
A2: t1 is_a_prefix_of t ;
assume t <> {} ; :: thesis: contradiction
then t1 is_a_proper_prefix_of t by A2;
then (tree_of_subformulae F) . t is_proper_subformula_of (tree_of_subformulae F) . t1 by Th16;
hence contradiction by A1, Def2; :: thesis: verum

end;

hence ( (tree_of_subformulae F) . t = F implies t = {} ) ; :: thesis: ( t = {} implies (tree_of_subformulae F) . t = F )
assume t = {} ; :: thesis: (tree_of_subformulae F) . t = F
hence (tree_of_subformulae F) . t = F by Def2; :: thesis: verum