let R be finite RelStr ; :: thesis: stability# R <= card the carrier of R
consider C being finite StableSet of R such that
A: card C = stability# R by DILWORTH:def 6;
card C c= card the carrier of R by CARD_1:27;
hence stability# R <= card the carrier of R by A, NAT_1:40; :: thesis: verum