let p be Element of CQC-WFF ; :: thesis: SepVar ('not' p) = 'not' (SepVar p)
reconsider FP = SepFunc . p as Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
thus SepVar ('not' p) = (NEGATIVE FP) . [(index ('not' p)),(id bound_QC-variables )] by Def6
.= (NEGATIVE FP) . [(index p),(id bound_QC-variables )] by Th24
.= 'not' (SepVar p) by Def1 ; :: thesis: verum