let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st F is_subformula_of H holds
Subformulae F c= Subformulae H
let F, H be Element of QC-WFF A; :: thesis: ( F is_subformula_of H implies Subformulae F c= Subformulae H )
assume A1: F is_subformula_of H ; :: thesis: Subformulae F c= Subformulae H
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae F or a in Subformulae H )
assume a in Subformulae F ; :: thesis: a in Subformulae H
then consider F1 being Element of QC-WFF A such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def22;
F1 is_subformula_of H by A1, A3, Th57;
hence a in Subformulae H by A2, Def22; :: thesis: verum