let p be Element of QC-WFF ; :: thesis: ( 'not' p is Element of CQC-WFF iff p is Element of CQC-WFF )
thus ( 'not' p is Element of CQC-WFF implies p is Element of CQC-WFF ) :: thesis: ( p is Element of CQC-WFF implies 'not' p is Element of CQC-WFF )

proof

assume A1: 'not' p is Element of CQC-WFF ; :: thesis: p is Element of CQC-WFF
then Free ('not' p) = {} by Th13;
then A2: Free p = {} by QC_LANG3:55;
Fixed ('not' p) = {} by A1, Th13;
then Fixed p = {} by QC_LANG3:65;
hence p is Element of CQC-WFF by A2, Th13; :: thesis: verum

end;

assume p is Element of CQC-WFF ; :: thesis: 'not' p is Element of CQC-WFF
then reconsider r = p as Element of CQC-WFF ;
Fixed r = {} by Th13;
then A3: Fixed ('not' r) = {} by QC_LANG3:65;
Free r = {} by Th13;
then Free ('not' r) = {} by QC_LANG3:55;
hence 'not' p is Element of CQC-WFF by A3, Th13; :: thesis: verum