let F, G, H be Element of QC-WFF ; :: 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 t' being Element of dom (tree_of_subformulae F) such that
A3: G = (tree_of_subformulae F) . t' and
A4: t' in C by A1;
consider t'' being Element of dom (tree_of_subformulae F) such that
A5: H = (tree_of_subformulae F) . t'' and
A6: t'' in C by A2;
A7: t',t'' are_c=-comparable by A4, A6, TREES_2:def 3;

per cases ( t' is_a_prefix_of t'' or t'' is_a_prefix_of t' ) by A7, XBOOLE_0:def 9;

suppose t' is_a_prefix_of t'' ; :: thesis: ( G is_subformula_of H or H is_subformula_of G )

hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th42; :: thesis: verum

end;

suppose t'' is_a_prefix_of t' ; :: thesis: ( G is_subformula_of H or H is_subformula_of G )

hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th42; :: thesis: verum

end;

end;