:: deftheorem Def9 defines Mycielskian MYCIELSK:def 9 :
for n being Nat
for R being NatRelStr of n
for b₃ being NatRelStr of (2 * n) + 1 holds
( b₃ = Mycielskian R iff the InternalRel of b₃ = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] );