let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A holds
( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A )
let p be Element of QC-WFF A; :: thesis: ( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A )
thus ( 'not' p is Element of CQC-WFF A implies p is Element of CQC-WFF A ) :: thesis: ( p is Element of CQC-WFF A implies 'not' p is Element of CQC-WFF A )
proof
assume A1: 'not' p is Element of CQC-WFF A ; :: thesis: p is Element of CQC-WFF A
then Free ('not' p) = {} by Th4;
then A2: Free p = {} by QC_LANG3:55;
Fixed ('not' p) = {} by A1, Th4;
then Fixed p = {} by QC_LANG3:65;
hence p is Element of CQC-WFF A by A2, Th4; :: thesis: verum
end;
assume p is Element of CQC-WFF A ; :: thesis: 'not' p is Element of CQC-WFF A
then reconsider r = p as Element of CQC-WFF A ;
Fixed r = {} by Th4;
then A3: Fixed ('not' r) = {} by QC_LANG3:65;
Free r = {} by Th4;
then Free ('not' r) = {} by QC_LANG3:55;
hence 'not' p is Element of CQC-WFF A by A3, Th4; :: thesis: verum