:: deftheorem Def22 defines -formulasOfMaxDepth FOMODEL2:def 23 :
for S being Language
for m being natural Number
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
for mm being Element of NAT st m = mm holds
b₃ = dom ((I,mm) -TruthEval) );