let F, H be ZF-formula; :: thesis: ( F is_immediate_constituent_of 'not' H iff F = H )
thus ( F is_immediate_constituent_of 'not' H implies F = H ) :: thesis: ( F = H implies F is_immediate_constituent_of 'not' H )

proof

assume F is_immediate_constituent_of 'not' H ; :: thesis: F = H
then A1: ( 'not' H = 'not' F or ex H1 being ZF-formula st
( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) or ex x being Variable st 'not' H = All x,F ) by Def39;

A2: now

given H1 being ZF-formula such that A3: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; :: thesis: contradiction
( ('not' H) . 1 = 2 & (F '&' H1) . 1 = 3 & (H1 '&' F) . 1 = 3 ) by Th33, FINSEQ_1:58;
hence contradiction by A3; :: thesis: verum

end;

now

given x being Variable such that A4: 'not' H = All x,F ; :: thesis: contradiction
( ('not' H) . 1 = 2 & (All x,F) . 1 = 4 ) by Th34, FINSEQ_1:58;
hence contradiction by A4; :: thesis: verum

end;

hence F = H by A1, A2, FINSEQ_1:46; :: thesis: verum

end;

thus ( F = H implies F is_immediate_constituent_of 'not' H ) by Def39; :: thesis: verum