let n be Nat; :: thesis: ex G being finite SimpleGraph st
( stability# G = 2 & cliquecover# G > n )
set G = (MycielskianSeq (CompleteSGraph 2)) . n;
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
then A1: ( clique# ((MycielskianSeq (CompleteSGraph 2)) . n) = 2 & chromatic# ((MycielskianSeq (CompleteSGraph 2)) . n) > n ) by Th118;
take S = Complement ((MycielskianSeq (CompleteSGraph 2)) . n); :: thesis: ( stability# S = 2 & cliquecover# S > n )
thus stability# S = 2 by A1, Th76; :: thesis: cliquecover# S > n
thus cliquecover# S > n by A1, Th82; :: thesis: verum