let F, G, H be ZF-formula; :: thesis: ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) )
( F is_immediate_constituent_of F '&' G & G is_immediate_constituent_of F '&' G ) by ZF_LANG:def 39;
hence ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th44; :: thesis: verum