theorem Th89: :: SCMYCIEL:89

for G being finite SimpleGraph holds order (Mycielskian G) = (2 * (order G)) + 1