let R be with_finite_stability# RelStr ; :: thesis: for S being Subset of R holds stability# (subrelstr S) <= stability# R
let S be Subset of R; :: thesis: stability# (subrelstr S) <= stability# R
consider As being StableSet of (subrelstr S) such that
As: card As = stability# (subrelstr S) by Lwidth;
As is StableSet of R by SPAChain1;
hence stability# (subrelstr S) <= stability# R by As, Lwidth; :: thesis: verum