let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )
let F, G, H be Element of QC-WFF A; :: 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 Th69;
hence ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th63; :: thesis: verum