theorem :: ZF_LANG1:47

for F, G, H being ZF-formula st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )