consider A being finite StableSet of R such that
A: for B being finite StableSet of R holds card A >= card B by Lfwidth;
assume Aa: not subrelstr S is with_finite_stability# ; :: thesis: contradiction
defpred S₁[ Nat] means ex C being finite StableSet of (subrelstr S) st
( card C = R & ex B being finite StableSet of (subrelstr S) st R < card B );
P1: S₁[ 0 ]

proof

reconsider C = {} (subrelstr S) as finite StableSet of (subrelstr S) ;
take C ; :: thesis: ( card C = 0 & ex B being finite StableSet of (subrelstr S) st 0 < card B )
thus card C = 0 ; :: thesis: ex B being finite StableSet of (subrelstr S) st 0 < card B
hence ex B being finite StableSet of (subrelstr S) st 0 < card B by Aa, Lfwidth; :: thesis: verum

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
given C being finite StableSet of (subrelstr S) such that card C = n and
C1: ex B being finite StableSet of (subrelstr S) st n < card B ; :: thesis: S₁[n + 1]
consider B being finite Subset of (subrelstr S) such that
D1: ( n < card B & B is StableSet of (subrelstr S) ) by C1;
n + 1 <= card B by D1, NAT_1:13;
then consider BB being finite StableSet of (subrelstr S) such that
E1: card BB = n + 1 by D1, AChain1;
take BB ; :: thesis: ( card BB = n + 1 & ex B being finite StableSet of (subrelstr S) st n + 1 < card B )
thus card BB = n + 1 by E1; :: thesis: ex B being finite StableSet of (subrelstr S) st n + 1 < card B
consider Bb being finite StableSet of (subrelstr S) such that
D1b: card BB < card Bb by Aa, Lfwidth;
take Bb ; :: thesis: n + 1 < card Bb
thus n + 1 < card Bb by D1b, E1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
then consider C being finite StableSet of (subrelstr S) such that
card C = card A and
S: ex B being finite StableSet of (subrelstr S) st card A < card B ;
consider B being finite StableSet of (subrelstr S) such that
T: card A < card B by S;
B is StableSet of R by SPAChain1;
hence contradiction by A, T; :: thesis: verum