theorem Th43: :: MYCIELSK:43

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