let n be Nat; :: thesis: 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
let R be NatRelStr of n; :: thesis: 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
let a, b be set ; :: thesis: ( a in Segm n & b in Segm n & [a,b] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R )
assume that
A1: a in Segm n and
A2: b in Segm n and
A3: [a,b] in the InternalRel of (Mycielskian R) ; :: thesis: [a,b] in the InternalRel of R
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A4: 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 Def9;

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

suppose [a,b] in the InternalRel of R ; :: thesis: [a,b] in the InternalRel of R

hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

suppose [a,b] 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
A5: [a,b] = [x,(y + n)] and
[x,y] in the InternalRel of R ;
b = y + n by A5, XTUPLE_0:1;
then y + n < n by A2, NAT_1:44;
then y < n - n by XREAL_1:20;
then y < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

suppose [a,b] 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
A6: [a,b] = [(x + n),y] and
[x,y] in the InternalRel of R ;
a = x + n by A6, XTUPLE_0:1;
then x + n < n by A1, NAT_1:44;
then x < n - n by XREAL_1:20;
then x < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

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

then consider c, d being object such that
A7: c in {(2 * n)} and
d in (2 * n) \ n and
A8: [a,b] = [c,d] by ZFMISC_1:def 2;
A9: c = 2 * n by A7, TARSKI:def 1;
A10: c = a by A8, XTUPLE_0:1;
n + n < n by A1, A10, A9, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

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

then consider c, d being object such that
c in (2 * n) \ n and
A11: d in {(2 * n)} and
A12: [a,b] = [c,d] by ZFMISC_1:def 2;
A13: d = 2 * n by A11, TARSKI:def 1;
A14: d = b by A12, XTUPLE_0:1;
n + n < n by A2, A14, A13, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum

end;

end;