let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds
not t,t9 are_c=-comparable
let F be Element of QC-WFF A; :: thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds
not t,t9 are_c=-comparable
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 implies not t,t9 are_c=-comparable )
assume that
A1: t <> t9 and
A2: (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 ; :: thesis: not t,t9 are_c=-comparable
assume A3: t,t9 are_c=-comparable ; :: thesis: contradiction
per cases ( t is_a_prefix_of t9 or t9 is_a_prefix_of t ) by A3;
suppose t is_a_prefix_of t9 ; :: thesis: contradiction
then t is_a_proper_prefix_of t9 by A1;
hence contradiction by A2, Th16; :: thesis: verum
end;
suppose t9 is_a_prefix_of t ; :: thesis: contradiction
then t9 is_a_proper_prefix_of t by A1;
hence contradiction by A2, Th16; :: thesis: verum
end;
end;