let n be Nat; :: thesis: for R being NatRelStr of n
for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let R be NatRelStr of n; :: thesis: for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let a, b be Nat; :: thesis: ( a in n & [a,(b + n)] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R )
set cR = the carrier of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
assume that
A: a in n and
C: [a,(b + n)] in the InternalRel of (Mycielskian R) ; :: thesis: [a,b] in the InternalRel of R
D: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by LMR;

per cases ( [a,(b + n)] in the InternalRel of R or [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] or [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ) by C, D, U5;

suppose [a,(b + n)] in the InternalRel of R ; :: thesis: [a,b] in the InternalRel of R

then b + n in the carrier of R by ZFMISC_1:106;
then b + n in n by LNRS;
then b + n < n by NAT_1:45;
then b < n - n by XREAL_1:22;
then b < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

suppose [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; :: thesis: [a,b] in the InternalRel of R

then consider x, y being Element of NAT such that
A1: [a,(b + n)] = [x,(y + n)] and
B1: [x,y] in the InternalRel of R ;
b + n = y + n by A1, ZFMISC_1:33;
hence [a,b] in the InternalRel of R by B1, A1, ZFMISC_1:33; :: thesis: verum

end;

suppose [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; :: thesis: [a,b] in the InternalRel of R

then consider x, y being Element of NAT such that
A1: [a,(b + n)] = [(x + n),y] and
B1: [x,y] in the InternalRel of R ;
b + n = y by A1, ZFMISC_1:33;
then b + n in the carrier of R by B1, ZFMISC_1:106;
then b + n in n by LNRS;
then b + n < n by NAT_1:45;
then b < n - n by XREAL_1:22;
then b < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

suppose [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] ; :: thesis: [a,b] in the InternalRel of R

then consider c, d being set such that
A1: c in {(2 * n)} and
d in (2 * n) \ n and
C1: [a,(b + n)] = [c,d] by ZFMISC_1:def 2;
D1: c = 2 * n by A1, TARSKI:def 1;
E1: c = a by C1, ZFMISC_1:33;
n + n < n by A, E1, D1, NAT_1:45;
then n < n - n by XREAL_1:22;
then n < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

suppose [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ; :: thesis: [a,b] in the InternalRel of R

then consider c, d being set such that
A1: c in (2 * n) \ n and
d in {(2 * n)} and
C1: [a,(b + n)] = [c,d] by ZFMISC_1:def 2;
c = a by C1, ZFMISC_1:33;
then n <= a by A1, Nat0;
hence [a,b] in the InternalRel of R by A, NAT_1:45; :: thesis: verum

end;

end;