:: deftheorem Def30 defines Depth FOMODEL2:def 31 :
for S being Language
for phi being wff string of S
for b₃ being Nat holds
( b₃ = Depth phi iff ( phi is b₃ -wff & ( for n being Nat st phi is n -wff holds
b₃ <= n ) ) );