consider E being Coloring of (Mycielskian G) such that
A1: card E = 1 + (chromatic# G) by Th111;
E is finite by A1;
hence Mycielskian G is finitely_colorable ; :: thesis: verum