set CR = ComplRelStr R;
consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by DILWORTH:def 3;
assume not ComplRelStr R is with_finite_stability# ; :: thesis: contradiction
then A2: for A being finite StableSet of (ComplRelStr R) ex B being finite StableSet of (ComplRelStr R) st card B > card A ;
defpred S2[ Nat] means ex S being finite StableSet of (ComplRelStr R) st card S > R;
consider B being finite StableSet of (ComplRelStr R) such that
A3: card B > card ({} (ComplRelStr R)) by A2;
A4: S2[ 0 ] by A3;
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume S2[n] ; :: thesis: S2[n + 1]
then consider S being finite StableSet of (ComplRelStr R) such that
A6: card S > n ;
consider T being finite StableSet of (ComplRelStr R) such that
A7: card T > card S by A2;
card S >= n + 1 by A6, NAT_1:13;
then card T > n + 1 by A7, XXREAL_0:2;
hence S2[n + 1] ; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A4, A5);
 then consider S being finite StableSet of (ComplRelStr R) such that
A8: card S > card C ;
S is Clique of R by Th22;
hence contradiction by A1, A8; :: thesis: verum