let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A holds
( F is_immediate_constituent_of 'not' H iff F = H )
let F, H be Element of QC-WFF A; :: 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

'not' H is negative by QC_LANG1:def 19;
then A1: ((@ ('not' H)) . 1) `1 = 1 by QC_LANG1:18;

A2: now :: thesis: for H1 being Element of QC-WFF A holds
( not 'not' H = F '&' H1 & not 'not' H = H1 '&' F )

given H1 being Element of QC-WFF A such that A3: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; :: thesis: contradiction
( F '&' H1 is conjunctive & H1 '&' F is conjunctive ) by QC_LANG1:def 20;
hence contradiction by A1, A3, QC_LANG1:18; :: thesis: verum

end;

A4: now :: thesis: for x being bound_QC-variable of A holds not 'not' H = All (x,F)

given x being bound_QC-variable of A such that A5: 'not' H = All (x,F) ; :: thesis: contradiction
All (x,F) is universal by QC_LANG1:def 21;
hence contradiction by A1, A5, QC_LANG1:18; :: thesis: verum

end;

assume ( 'not' H = 'not' F or ex H1 being Element of QC-WFF A st
( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) or ex x being bound_QC-variable of A st 'not' H = All (x,F) ) ; :: according to QC_LANG2:def 19 :: thesis: F = H
hence F = H by A2, A4, FINSEQ_1:33; :: thesis: verum

end;

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