:: deftheorem Def6 defines stability# DILWORTH:def 6 :
for R being with_finite_stability# RelStr
for b₂ being Nat holds
( b₂ = stability# R iff ( ex A being finite StableSet of R st card A = b₂ & ( for T being finite StableSet of R holds card T <= b₂ ) ) );