let R be with_finite_stability# RelStr ; :: thesis: for A being StableSet of R
for S being Subset of R st card A = stability# R & A c= S holds
stability# (subrelstr S) = stability# R
let A be StableSet of R; :: thesis: for S being Subset of R st card A = stability# R & A c= S holds
stability# (subrelstr S) = stability# R
let S be Subset of R; :: thesis: ( card A = stability# R & A c= S implies stability# (subrelstr S) = stability# R )
assume that
A: card A = stability# R and
B: A c= S ; :: thesis: stability# (subrelstr S) = stability# R
A = A /\ S by B, XBOOLE_1:28;
then C: A is StableSet of (subrelstr S) by SPAChain;
consider As being StableSet of (subrelstr S) such that
As: card As = stability# (subrelstr S) by Lwidth;
D: card A <= card As by C, As, Lwidth;
stability# (subrelstr S) <= stability# R by Wsubp0;
hence stability# (subrelstr S) = stability# R by As, A, D, XXREAL_0:1; :: thesis: verum