theorem Th57: :: ZF_LANG:57

for F, H being ZF-formula st H is conjunctive holds
( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )