theorem Th56: :: ZF_LANG:56

for F, H being ZF-formula st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )