let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H
let F, G, H be Element of QC-WFF A; :: thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H )
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H ; :: thesis: F is_subformula_of H
now :: thesis: ( F <> G implies F is_subformula_of H )
assume F <> G ; :: thesis: F is_subformula_of H
then A3: F is_proper_subformula_of G by A1;
now :: thesis: ( G <> H implies F is_subformula_of H )
assume G <> H ; :: thesis: F is_subformula_of H
then G is_proper_subformula_of H by A2;
then F is_proper_subformula_of H by A3, Th56;
hence F is_subformula_of H ; :: thesis: verum
end;
hence F is_subformula_of H by A1; :: thesis: verum
end;
hence F is_subformula_of H by A2; :: thesis: verum