let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A
for C being Chain of dom (tree_of_subformulae F) st G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H holds
H is_subformula_of G
let F, G, H be Element of QC-WFF A; :: thesis: for C being Chain of dom (tree_of_subformulae F) st G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H holds
H is_subformula_of G
let C be Chain of dom (tree_of_subformulae F); :: thesis: ( G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H implies H is_subformula_of G )
assume that
A1: G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } and
A2: H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } ; :: thesis: ( G is_subformula_of H or H is_subformula_of G )
consider t9 being Element of dom (tree_of_subformulae F) such that
A3: G = (tree_of_subformulae F) . t9 and
A4: t9 in C by A1;
consider t99 being Element of dom (tree_of_subformulae F) such that
A5: H = (tree_of_subformulae F) . t99 and
A6: t99 in C by A2;
A7: t9,t99 are_c=-comparable by A4, A6, TREES_2:def 3;