set CR = ComplRelStr R;
consider C being finite StableSet of R such that
A: for D being finite StableSet of R holds card D <= card C by DILWORTH:def 5;
assume not ComplRelStr R is with_finite_clique# ; :: thesis: contradiction
then B: for C being finite Clique of (ComplRelStr R) ex D being finite Clique of (ComplRelStr R) st card D > card C by DILWORTH:def 3;
defpred S₁[ Nat] means ex S being finite Clique of (ComplRelStr R) st card S > R;
consider B being finite Clique 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 Clique of (ComplRelStr R) such that
A2: card S > n ;
consider T being finite Clique 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 Clique of (ComplRelStr R) such that
R: card S > card C ;
S is StableSet of R by CliComplSta;
hence contradiction by A, R; :: thesis: verum