:: deftheorem Def16 defines essential AOFA_L00:def 18 :
for J being Signature
for X being non empty set
for n being non empty Nat
for S being feasible b₁ -extension b₃ PC-correct AlgLangSignature over X holds
( S is essential iff ( the connectives of S .: ((n + 9) \ n) misses the carrier' of J & rng the quantifiers of S misses the carrier' of J & { the formula-sort of S, the program-sort of S} misses the carrier of J ) );