theorem Th113: :: SCMYCIEL:113

for G being SimpleGraph holds (MycielskianSeq G) . 0 = G