theorem Th25: :: AOFA_L00:26

for n being natural non empty number
for X being non empty set
for S being non empty non void b₁ PC-correct QC-correct QCLangSignature over X
for Q being language MSAlgebra over S holds
( {} in Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),Q) & ( for A being Formula of Q holds
( <*A*> in Args ((In (( the connectives of S . n), the carrier' of S)),Q) & ( for B being Formula of Q holds
( <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),Q) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),Q) & ( for x being Element of X holds
( <*A*> in Args ((In (( the quantifiers of S . (1,x)), the carrier' of S)),Q) & <*A*> in Args ((In (( the quantifiers of S . (2,x)), the carrier' of S)),Q) ) ) ) ) ) ) )