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