theorem Th112: :: SCMYCIEL:112

for G being finitely_colorable SimpleGraph holds chromatic# (Mycielskian G) = 1 + (chromatic# G)