let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds SepVar ('not' p) = 'not' (SepVar p)
let p be Element of CQC-WFF A; :: thesis: SepVar ('not' p) = 'not' (SepVar p)
reconsider FP = (SepFunc A) . p as Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) ;
thus SepVar ('not' p) = (NEGATIVE FP) . [(index ('not' p)),(id (bound_QC-variables A))] by Def7
.= (NEGATIVE FP) . [(index p),(id (bound_QC-variables A))] by Th23
.= 'not' (SepVar p) by Def2 ; :: thesis: verum