let n be Nat; :: thesis: ex R being finite RelStr st
( stability# R = 2 & cliquecover# R > n )
set R = Mycielskian n;
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
then A1: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50;
take S = ComplRelStr (Mycielskian n); :: thesis: ( stability# S = 2 & cliquecover# S > n )
thus stability# S = 2 by A1, Th23; :: thesis: cliquecover# S > n
thus cliquecover# S > n by A1, Th29; :: thesis: verum