for n being Nat
for R being NatRelStr of n
for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )