:: deftheorem Def10 defines Mycielskian MYCIELSK:def 10 :
for n being Nat
for b₂ being NatRelStr of (3 * (2 |^ n)) -' 1 holds
( b₂ = Mycielskian n iff ex myc being Function st
( b₂ = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) ) );