let F be Element of QC-WFF ; :: thesis: for t, t' being Element of dom (tree_of_subformulae F) st t <> t' & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t' holds
not t,t' are_c=-comparable
let t, t' be Element of dom (tree_of_subformulae F); :: thesis: ( t <> t' & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t' implies not t,t' are_c=-comparable )
assume that
A1: t <> t' and
A2: (tree_of_subformulae F) . t = (tree_of_subformulae F) . t' ; :: thesis: not t,t' are_c=-comparable
assume A3: t,t' are_c=-comparable ; :: thesis: contradiction

per cases ( t is_a_prefix_of t' or t' is_a_prefix_of t ) by A3, XBOOLE_0:def 9;

suppose t is_a_prefix_of t' ; :: thesis: contradiction

then t is_a_proper_prefix_of t' by A1, XBOOLE_0:def 8;
hence contradiction by A2, Th45; :: thesis: verum

end;

suppose t' is_a_prefix_of t ; :: thesis: contradiction

then t' is_a_proper_prefix_of t by A1, XBOOLE_0:def 8;
hence contradiction by A2, Th45; :: thesis: verum

end;

end;