let p be Element of QC-WFF ; :: thesis: the_argument_of ('not' p) = p
'not' p is negative by QC_LANG1:def 18;
hence the_argument_of ('not' p) = p by QC_LANG1:def 23; :: thesis: verum