set cR = the carrier of R;
set iR = the InternalRel of R;
set cMR = (2 * n) + 1;
set iMR = ((( 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)}:];
A1: the carrier of R = n by Def7;
n <= n + n by NAT_1:11;
then A2: n < (2 * n) + 1 by NAT_1:13;
((( 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)}:] c= [:((2 * n) + 1),((2 * n) + 1):]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ((( 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)}:] or z in [:((2 * n) + 1),((2 * n) + 1):] )
assume A3: z in ((( 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)}:] ; :: thesis: z in [:((2 * n) + 1),((2 * n) + 1):]

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

suppose z in the InternalRel of R ; :: thesis: z in [:((2 * n) + 1),((2 * n) + 1):]

then consider c, d being object such that
A4: c in Segm n and
A5: d in Segm n and
A6: z = [c,d] by ZFMISC_1:def 2, A1;
reconsider c = c, d = d as Nat by A4, A5;
( c < n & d < n ) by A4, A5, NAT_1:44;
then ( c < (2 * n) + 1 & d < (2 * n) + 1 ) by A2, XXREAL_0:2;
then ( c in Segm ((2 * n) + 1) & d in Segm ((2 * n) + 1) ) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A6, ZFMISC_1:def 2; :: thesis: verum

end;

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

then consider x, y being Element of NAT such that
A7: z = [x,(y + n)] and
A8: [x,y] in the InternalRel of R ;
x in Segm n by A1, A8, ZFMISC_1:87;
then x < n by NAT_1:44;
then x < (2 * n) + 1 by A2, XXREAL_0:2;
then A9: x in Segm ((2 * n) + 1) by NAT_1:44;
y in Segm n by A1, A8, ZFMISC_1:87;
then y < n by NAT_1:44;
then y + n < n + n by XREAL_1:6;
then y + n < (2 * n) + 1 by NAT_1:13;
then y + n in Segm ((2 * n) + 1) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A7, A9, ZFMISC_1:def 2; :: thesis: verum

end;

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

then consider x, y being Element of NAT such that
A10: z = [(x + n),y] and
A11: [x,y] in the InternalRel of R ;
y in Segm n by A1, A11, ZFMISC_1:87;
then y < n by NAT_1:44;
then y < (2 * n) + 1 by A2, XXREAL_0:2;
then A12: y in Segm ((2 * n) + 1) by NAT_1:44;
x in Segm n by A1, A11, ZFMISC_1:87;
then x < n by NAT_1:44;
then x + n < n + n by XREAL_1:6;
then x + n < (2 * n) + 1 by NAT_1:13;
then x + n in Segm ((2 * n) + 1) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A10, A12, ZFMISC_1:def 2; :: thesis: verum

end;

suppose z in [:{(2 * n)},((2 * n) \ n):] ; :: thesis: z in [:((2 * n) + 1),((2 * n) + 1):]

then consider c, d being object such that
A13: c in {(2 * n)} and
A14: d in (Segm (2 * n)) \ (Segm n) and
A15: z = [c,d] by ZFMISC_1:def 2;
A16: c = 2 * n by A13, TARSKI:def 1;
reconsider c = c as Nat by A13, TARSKI:def 1;
c < (2 * n) + 1 by A16, NAT_1:13;
then A17: c in Segm ((2 * n) + 1) by NAT_1:44;
reconsider d = d as Nat by A14;
d < 2 * n by A14, Th2;
then d < (2 * n) + 1 by NAT_1:13;
then d in Segm ((2 * n) + 1) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A17, A15, ZFMISC_1:def 2; :: thesis: verum

end;

suppose z in [:((2 * n) \ n),{(2 * n)}:] ; :: thesis: z in [:((2 * n) + 1),((2 * n) + 1):]

then consider c, d being object such that
A18: c in (Segm (2 * n)) \ (Segm n) and
A19: d in {(2 * n)} and
A20: z = [c,d] by ZFMISC_1:def 2;
A21: d = 2 * n by A19, TARSKI:def 1;
reconsider d = d as Nat by A19, TARSKI:def 1;
d < (2 * n) + 1 by A21, NAT_1:13;
then A22: d in Segm ((2 * n) + 1) by NAT_1:44;
reconsider c = c as Nat by A18;
c < 2 * n by A18, Th2;
then c < (2 * n) + 1 by NAT_1:13;
then c in Segm ((2 * n) + 1) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A22, A20, ZFMISC_1:def 2; :: thesis: verum

end;

end;

end;

then reconsider iMR = ((( 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)}:] as Relation of ((2 * n) + 1) ;
set MR = RelStr(# ((2 * n) + 1),iMR #);
take RelStr(# ((2 * n) + 1),iMR #) ; :: thesis: ( RelStr(# ((2 * n) + 1),iMR #) is NatRelStr of (2 * n) + 1 & the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:] )
thus the carrier of RelStr(# ((2 * n) + 1),iMR #) = (2 * n) + 1 ; :: according to MYCIELSK:def 7 :: thesis: the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:]
thus the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:] ; :: thesis: verum