let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds
CQC_Sub (Sub_not S) is Element of CQC-WFF A
let S be Element of QC-Sub-WFF A; :: thesis: ( CQC_Sub S is Element of CQC-WFF A implies CQC_Sub (Sub_not S) is Element of CQC-WFF A )
set S9 = Sub_not S;
assume A1: CQC_Sub S is Element of CQC-WFF A ; :: thesis: CQC_Sub (Sub_not S) is Element of CQC-WFF A
CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th29;
hence CQC_Sub (Sub_not S) is Element of CQC-WFF A by A1, CQC_LANG:8; :: thesis: verum