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