let n be Nat; :: thesis: ex G being finite SimpleGraph st
( clique# G = 2 & chromatic# G > n )
set P2 = CompleteSGraph 2;
reconsider G = (MycielskianSeq (CompleteSGraph 2)) . n as finite SimpleGraph ;
take G ; :: thesis: ( clique# G = 2 & chromatic# G > n )
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
hence ( clique# G = 2 & chromatic# G > n ) by Th118; :: thesis: verum