let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
let S be Element of QC-Sub-WFF A; :: thesis: CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
set 9S = Sub_not S;
Sub_the_argument_of (Sub_not S) = S by Def30;
hence CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th28; :: thesis: verum