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 A1: ( 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 } ) ; :: thesis: ( G is_subformula_of H or H is_subformula_of G )
then consider t' being Element of dom (tree_of_subformulae F) such that
A2: ( G = (tree_of_subformulae F) . t' & t' in C ) ;
consider t'' being Element of dom (tree_of_subformulae F) such that
A3: ( H = (tree_of_subformulae F) . t'' & t'' in C ) by A1;
A4: t',t'' are_c=-comparable by A2, A3, TREES_2:def 3;

per cases ( t' is_a_prefix_of t'' or t'' is_a_prefix_of t' ) by A4, 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 A2, A3, 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 A2, A3, Th42; :: thesis: verum

end;

end;