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