let n be Nat; :: thesis: ex R being finite RelStr st
( clique# R = 2 & chromatic# R > n )
take Mycielskian n ; :: thesis: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n )
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
hence ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50; :: thesis: verum