theorem Th45: :: DILWORTH:45

for R being with_finite_stability# RelStr
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