let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A holds the_argument_of ('not' p) = p
let p be Element of QC-WFF A; :: thesis: the_argument_of ('not' p) = p
'not' p is negative ;
hence the_argument_of ('not' p) = p by QC_LANG1:def 24; :: thesis: verum