:: deftheorem Def5 defines with_finite_stability# DILWORTH:def 5 :
for R being RelStr holds
( R is with_finite_stability# iff ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A );