let A be QC-alphabet ; :: thesis: for G, H being Element of QC-WFF A st G in Subformulae H holds
G is_subformula_of H
let G, H be Element of QC-WFF A; :: thesis: ( G in Subformulae H implies G is_subformula_of H )
assume G in Subformulae H ; :: thesis: G is_subformula_of H
then ex F being Element of QC-WFF A st
( F = G & F is_subformula_of H ) by Def22;
hence G is_subformula_of H ; :: thesis: verum