for G, H being SimpleGraph
for n being Nat holds (MycielskianSeq G) . (n + 1) = Mycielskian ((MycielskianSeq G) . n)