for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )