let F be Element of QC-WFF ; :: thesis: for t, t' being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t' holds
(tree_of_subformulae F) . t' <> (tree_of_subformulae F) . t
let t, t' be Element of dom (tree_of_subformulae F); :: thesis: ( t is_a_proper_prefix_of t' implies (tree_of_subformulae F) . t' <> (tree_of_subformulae F) . t )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t';
assume t is_a_proper_prefix_of t' ; :: thesis: (tree_of_subformulae F) . t' <> (tree_of_subformulae F) . t
then len (@ ((tree_of_subformulae F) . t')) < len (@ ((tree_of_subformulae F) . t)) by Th43;
hence (tree_of_subformulae F) . t' <> (tree_of_subformulae F) . t ; :: thesis: verum