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