theorem Th48: :: MYCIELSK:48
for n being Nat
for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)