theorem Th111: :: SCMYCIEL:111

for G being finitely_colorable SimpleGraph ex E being Coloring of (Mycielskian G) st card E = 1 + (chromatic# G)