:: deftheorem defines \for AOFA_L00:def 28 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding b₄ -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x being Element of Union X holds \for (x,A) = (Den ((In (( the quantifiers of S . (1,x)), the carrier' of S)),L)) . <*A*>;