let R be RelStr ; :: thesis: ( R is finite implies R is with_finite_stability# )
assume R is finite ; :: thesis: R is with_finite_stability#
then reconsider R9 = R as finite RelStr ;
defpred S₁[ Nat] means ex A being finite StableSet of R9 st card A = c₁;
P1: for k being Nat st S₁[k] holds
k <= card R9 by NAT_1:44;
( {} R is StableSet of R & card {} = 0 ) ;
then P2: ex k being Nat st S₁[k] ;
consider k being Nat such that
A1: S₁[k] and
B1: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(P1, P2);
consider S being finite StableSet of R such that
C1: card S = k by A1;
take S ; :: according to DILWORTH:def 5 :: thesis: for B being finite StableSet of R holds card B <= card S
let T be finite StableSet of R; :: thesis: card T <= card S
thus card T <= card S by C1, B1; :: thesis: verum