theorem Th52: :: ZF_LANG:52

for F, H being ZF-formula holds
( F is_immediate_constituent_of 'not' H iff F = H )