:: deftheorem defines \not AOFA_L00:def 23 :
for n being natural non empty number
for S being non empty non void b₁ PC-correct PCLangSignature
for L being language MSAlgebra over S
for A being Formula of L holds \not A = (Den ((In (( the connectives of S . n), the carrier' of S)),L)) . <*A*>;