let n be Nat; :: thesis: for R being NatRelStr of n
for x, y being Nat st y in Segm n & [(x + n),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 Nat st y in Segm n & [(x + n),y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let a, b be Nat; :: thesis: ( b in Segm n & [(a + n),b] 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
A1: b in Segm n and
A2: [(a + n),b] in the InternalRel of (Mycielskian R) ; :: thesis: [a,b] in the InternalRel of R
A3: 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 + n),b] in the InternalRel of R or [(a + n),b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] or [(a + n),b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A3, Th4;
suppose [(a + n),b] in the InternalRel of R ; :: thesis: [a,b] in the InternalRel of R
then a + n in the carrier of R by ZFMISC_1:87;
then a + n in Segm n by Def7;
then a + n < n by NAT_1:44;
then a < n - n by XREAL_1:20;
then a < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum
end;
suppose [(a + n),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
A4: [(a + n),b] = [x,(y + n)] and
A5: [x,y] in the InternalRel of R ;
a + n = x by A4, XTUPLE_0:1;
then a + n in the carrier of R by A5, ZFMISC_1:87;
then a + n in Segm n by Def7;
then a + n < n by NAT_1:44;
then a < n - n by XREAL_1:20;
then a < 0 ;
hence [a,b] in the InternalRel of R ; :: thesis: verum
end;
suppose [(a + n),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 + n),b] = [(x + n),y] and
A7: [x,y] in the InternalRel of R ;
a + n = x + n by A6, XTUPLE_0:1;
hence [a,b] in the InternalRel of R by A7, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] ; :: thesis: [a,b] in the InternalRel of R
then consider c, d being object such that
c in {(2 * n)} and
A8: d in (Segm (2 * n)) \ (Segm n) and
A9: [(a + n),b] = [c,d] by ZFMISC_1:def 2;
b = d by A9, XTUPLE_0:1;
then n <= b by A8, Th2;
hence [a,b] in the InternalRel of R by A1, NAT_1:44; :: thesis: verum
end;
suppose [(a + n),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
A10: d in {(2 * n)} and
A11: [(a + n),b] = [c,d] by ZFMISC_1:def 2;
A12: d = 2 * n by A10, TARSKI:def 1;
d = b by A11, XTUPLE_0:1;
then n + n < n by A1, A12, 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;