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)}:];
B:
the carrier of R = n
by LNRS;
n <= n + n
by NAT_1:11;
then C:
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
set ;
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 A:
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 A, U5;
suppose
z in the
InternalRel of
R
;
z in [:((2 * n) + 1),((2 * n) + 1):]then consider c,
d being
set such that A1:
c in the
carrier of
R
and B1:
d in the
carrier of
R
and C1:
z = [c,d]
by ZFMISC_1:def 2;
reconsider c =
c,
d =
d as
Nat by B, A1, B1, NECKLACE:4;
(
c < n &
d < n )
by B, A1, B1, NAT_1:45;
then
(
c < (2 * n) + 1 &
d < (2 * n) + 1 )
by C, XXREAL_0:2;
then
(
c in (2 * n) + 1 &
d in (2 * n) + 1 )
by NAT_1:45;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by C1, 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 A1:
z = [x,(y + n)]
and B1:
[x,y] in the
InternalRel of
R
;
x in the
carrier of
R
by B1, ZFMISC_1:106;
then
x < n
by B, NAT_1:45;
then
x < (2 * n) + 1
by C, XXREAL_0:2;
then C1:
x in (2 * n) + 1
by NAT_1:45;
y in the
carrier of
R
by B1, ZFMISC_1:106;
then
y < n
by B, NAT_1:45;
then
y + n < n + n
by XREAL_1:8;
then
y + n < (2 * n) + 1
by NAT_1:13;
then
y + n in (2 * n) + 1
by NAT_1:45;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by A1, C1, 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 A1:
z = [(x + n),y]
and B1:
[x,y] in the
InternalRel of
R
;
y in the
carrier of
R
by B1, ZFMISC_1:106;
then
y < n
by B, NAT_1:45;
then
y < (2 * n) + 1
by C, XXREAL_0:2;
then C1:
y in (2 * n) + 1
by NAT_1:45;
x in the
carrier of
R
by B1, ZFMISC_1:106;
then
x < n
by B, NAT_1:45;
then
x + n < n + n
by XREAL_1:8;
then
x + n < (2 * n) + 1
by NAT_1:13;
then
x + n in (2 * n) + 1
by NAT_1:45;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by A1, C1, ZFMISC_1:def 2;
verum end; suppose
z in [:{(2 * n)},((2 * n) \ n):]
;
z in [:((2 * n) + 1),((2 * n) + 1):]then consider c,
d being
set such that A1:
c in {(2 * n)}
and B1:
d in (2 * n) \ n
and C1:
z = [c,d]
by ZFMISC_1:def 2;
D1:
c = 2
* n
by A1, TARSKI:def 1;
reconsider c =
c as
Nat by A1, TARSKI:def 1;
c < (2 * n) + 1
by D1, NAT_1:13;
then E1:
c in (2 * n) + 1
by NAT_1:45;
reconsider d =
d as
Nat by B1, NECKLACE:4;
d < 2
* n
by B1, Nat0;
then
d < (2 * n) + 1
by NAT_1:13;
then
d in (2 * n) + 1
by NAT_1:45;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by E1, C1, ZFMISC_1:def 2;
verum end; suppose
z in [:((2 * n) \ n),{(2 * n)}:]
;
z in [:((2 * n) + 1),((2 * n) + 1):]then consider c,
d being
set such that A1:
c in (2 * n) \ n
and B1:
d in {(2 * n)}
and C1:
z = [c,d]
by ZFMISC_1:def 2;
D1:
d = 2
* n
by B1, TARSKI:def 1;
reconsider d =
d as
Nat by B1, TARSKI:def 1;
d < (2 * n) + 1
by D1, NAT_1:13;
then E1:
d in (2 * n) + 1
by NAT_1:45;
reconsider c =
c as
Nat by A1, NECKLACE:4;
c < 2
* n
by A1, Nat0;
then
c < (2 * n) + 1
by NAT_1:13;
then
c in (2 * n) + 1
by NAT_1:45;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by E1, C1, 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