theorem Th42: :: MYCIELSK:42

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