:: deftheorem Def26 defines MycielskianSeq SCMYCIEL:def 26 :
for G being SimpleGraph
for b₂ being ManySortedSet of NAT holds
( b₂ = MycielskianSeq G iff ex myc being Function st
( b₂ = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) );