let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let F be Element of QC-WFF A; :: thesis: for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let G be Subformula of F; :: thesis: for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let t, t9 be Entry_Point_in_Subformula_Tree of G; :: thesis: ( t <> t9 implies not t,t9 are_c=-comparable )
assume A1: t <> t9 ; :: thesis: not t,t9 are_c=-comparable
( (tree_of_subformulae F) . t = G & (tree_of_subformulae F) . t9 = G ) by Def5;
hence not t,t9 are_c=-comparable by A1, Th18; :: thesis: verum