for R being with_finite_stability# RelStr
for S being Subset of R holds stability# (subrelstr S) <= stability# R