let S be Element of QC-Sub-WFF ; :: thesis: CQC_Sub (Sub_not S) = 'not' (CQC_Sub S)
set 'S = 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