:: deftheorem Def12 defines height TREES_1:def 12 :
for T being finite Tree
for b₂ being Nat holds
( b₂ = height T iff ( ex p being FinSequence of NAT st
( p in T & len p = b₂ ) & ( for p being FinSequence of NAT st p in T holds
len p <= b₂ ) ) );