:: deftheorem Def13 defines width TREES_1:def 13 :
for T being finite Tree
for b₂ being Nat holds
( b₂ = width T iff ex X being AntiChain_of_Prefixes of T st
( b₂ = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) );