theorem Th18: :: QC_LANG4:18

for A being QC-alphabet
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