:: deftheorem Def27 defines -formulasOfMaxDepth FOMODEL2:def 28 :
for S being Language
for m being Nat
for b₃ being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b₃ = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b₃ = dom ((I,m) -TruthEval) );