let F, G, H be Element of QC-WFF ; :: thesis: ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) )
( F is_proper_subformula_of F '&' G & G is_proper_subformula_of F '&' G ) by Th89;
hence ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th83; :: thesis: verum