:: deftheorem Def24 defines the_argument_of QC_LANG1:def 24 :
for A being QC-alphabet
for F being Element of QC-WFF A st F is negative holds
for b₃ being QC-formula of A holds
( b₃ = the_argument_of F iff F = 'not' b₃ );