theorem Th40: :: MYCIELSK:40

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