:: deftheorem Def40 defines Depth FOMODEL1:def 40 :
for S being Language
for t being termal string of S
for b₃ being Nat holds
( b₃ = Depth t iff ( t is b₃ -termal & ( for n being Nat st t is n -termal holds
b₃ <= n ) ) );