consider A being finite StableSet of R such that
A1: for B being finite StableSet of R holds card A >= card B by Def5;
assume A2: not subrelstr S is with_finite_stability# ; :: thesis: contradiction
defpred S1[ 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 );
A3: S1[ 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 A2; :: thesis: verum
end;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
given C being finite StableSet of (subrelstr S) such that card C = n and
A5: ex B being finite StableSet of (subrelstr S) st n < card B ; :: thesis: S1[n + 1]
consider B being finite Subset of (subrelstr S) such that
A6: ( n < card B & B is StableSet of (subrelstr S) ) by A5;
n + 1 <= card B by A6, NAT_1:13;
then consider BB being finite StableSet of (subrelstr S) such that
A7: card BB = n + 1 by A6, Th17;
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 A7; :: thesis: ex B being finite StableSet of (subrelstr S) st n + 1 < card B
consider Bb being finite StableSet of (subrelstr S) such that
A8: card BB < card Bb by A2;
take Bb ; :: thesis: n + 1 < card Bb
thus n + 1 < card Bb by A8, A7; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 then consider C being finite StableSet of (subrelstr S) such that
card C = card A and
A9: ex B being finite StableSet of (subrelstr S) st card A < card B ;
consider B being finite StableSet of (subrelstr S) such that
A10: card A < card B by A9;
B is StableSet of R by Th30;
hence contradiction by A1, A10; :: thesis: verum