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 ;
TARSKI:def 3 ( 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)}:]
;
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
;
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;
verum end; suppose
z in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R }
;
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;
verum end; suppose
z in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R }
;
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;
verum 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 #)
; ( 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
; MYCIELSK:def 7 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)}:]
; verum