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