for G being finite SimpleGraph holds size (Mycielskian G) = (3 * (size G)) + (order G)