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
A1: card A = stability# R and
A2: A c= S ; :: thesis: stability# (subrelstr S) = stability# R
A = A /\ S by A2, XBOOLE_1:28;
then A3: A is StableSet of (subrelstr S) by Th31;
consider As being StableSet of (subrelstr S) such that
A4: card As = stability# (subrelstr S) by Def6;
A5: card A <= card As by A3, A4, Def6;
stability# (subrelstr S) <= stability# R by Th44;
hence stability# (subrelstr S) = stability# R by A4, A1, A5, XXREAL_0:1; :: thesis: verum