:: deftheorem Def19 defines negative QC_LANG1:def 19 :
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is negative iff ex p being Element of QC-WFF A st F = 'not' p );