theorem Th38: :: MYCIELSK:38

for n being Nat
for R being NatRelStr of n
for x, y being Nat holds
( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )