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
A1: now :: thesis: for x being Variable holds not 'not' H = All (x,F)
given x being Variable such that A2: 'not' H = All (x,F) ; :: thesis: contradiction
('not' H) . 1 = 2 by FINSEQ_1:41;
hence contradiction by A2, Th17; :: thesis: verum
end;
A3: now :: thesis: for H1 being ZF-formula holds
( not 'not' H = F '&' H1 & not 'not' H = H1 '&' F )
given H1 being ZF-formula such that A4: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; :: thesis: contradiction
('not' H) . 1 = 2 by FINSEQ_1:41;
hence contradiction by A4, Th16; :: thesis: verum
end;
assume F is_immediate_constituent_of 'not' H ; :: thesis: F = H
then ( '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) ) ;
hence F = H by A3, A1, FINSEQ_1:33; :: thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of 'not' H ) ; :: thesis: verum