for G being SimpleGraph
for n being Nat holds (MycielskianSeq G) . n is SimpleGraph