theorem Th41: :: MYCIELSK:41

for n being Nat
for R being NatRelStr of n
for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )