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 ) ;
hence ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th40; :: thesis: verum