set CR = ComplRelStr R;
consider C being finite StableSet of R such that
A1: 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 A2: for C being finite Clique of (ComplRelStr R) ex D being finite Clique of (ComplRelStr R) st card D > card C ;
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
A3: card B > card ({} (ComplRelStr R)) by A2;
A4: S₂[ 0 ] by A3;
A5: 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
A6: card S > n ;
consider T being finite Clique 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 S₂[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A4, A5);
then consider S being finite Clique of (ComplRelStr R) such that
A8: card S > card C ;
S is StableSet of R by Th20;
hence contradiction by A1, A8; :: thesis: verum