for G being finite SimpleGraph
for n being Nat holds order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1