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
A1: card As = stability# (subrelstr S) by Def6;
As is StableSet of R by Th30;
hence stability# (subrelstr S) <= stability# R by A1, Def6; :: thesis: verum