set CR = ComplRelStr R;
consider C being finite Clique of R such that
A: 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 B: for A being finite StableSet of (ComplRelStr R) ex B being finite StableSet of (ComplRelStr R) st card B > card A by DILWORTH:def 5;
defpred S₁[ Nat] means ex S being finite StableSet of (ComplRelStr R) st card S > R;
consider B being finite StableSet of (ComplRelStr R) such that
A1: card B > card ({} (ComplRelStr R)) by B;
P0: S₁[ 0 ] by A1;
P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider S being finite StableSet of (ComplRelStr R) such that
A2: card S > n ;
consider T being finite StableSet of (ComplRelStr R) such that
B2: card T > card S by B;
card S >= n + 1 by A2, NAT_1:13;
then card T > n + 1 by B2, XXREAL_0:2;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
then consider S being finite StableSet of (ComplRelStr R) such that
R: card S > card C ;
S is Clique of R by StaComplCli;
hence contradiction by A, R; :: thesis: verum