let G, H be Element of QC-WFF ; :: 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 st
( F = G & F is_subformula_of H ) by Def23;
hence G is_subformula_of H ; :: thesis: verum