theorem :: ZF_LANG:74

for H being ZF-formula st H is conjunctive holds
( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )