:: deftheorem Def2 defines NEGATIVE CQC_SIM1:def 2 :
for A being QC-alphabet
for D being non empty set
for f being Function of D,(CQC-WFF A)
for b₄ being Element of Funcs (D,(CQC-WFF A)) holds
( b₄ = NEGATIVE f iff for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
b₄ . a = 'not' p );