for R being with_finite_stability# RelStr
for A being StableSet of R st card A = stability# R holds
(Upper A) \/ (Lower A) = [#] R