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
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 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
set such that A4:
c in the
carrier of
R
and A5:
d in the
carrier of
R
and A6:
z = [c,d]
by ZFMISC_1:def 2;
reconsider c =
c,
d =
d as
Nat by A1, A4, A5, NECKLACE:3;
(
c < n &
d < n )
by A1, A4, A5, NAT_1:44;
then
(
c < (2 * n) + 1 &
d < (2 * n) + 1 )
by A2, XXREAL_0:2;
then
(
c in (2 * n) + 1 &
d in (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 the
carrier of
R
by A8, ZFMISC_1:87;
then
x < n
by A1, NAT_1:44;
then
x < (2 * n) + 1
by A2, XXREAL_0:2;
then A9:
x in (2 * n) + 1
by NAT_1:44;
y in the
carrier of
R
by A8, ZFMISC_1:87;
then
y < n
by A1, 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 (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 the
carrier of
R
by A11, ZFMISC_1:87;
then
y < n
by A1, NAT_1:44;
then
y < (2 * n) + 1
by A2, XXREAL_0:2;
then A12:
y in (2 * n) + 1
by NAT_1:44;
x in the
carrier of
R
by A11, ZFMISC_1:87;
then
x < n
by A1, 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 (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; suppose
z in [:{(2 * n)},((2 * n) \ n):]
;
z in [:((2 * n) + 1),((2 * n) + 1):]then consider c,
d being
set such that A13:
c in {(2 * n)}
and A14:
d in (2 * n) \ 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 (2 * n) + 1
by NAT_1:44;
reconsider d =
d as
Nat by A14, NECKLACE:3;
d < 2
* n
by A14, Th2;
then
d < (2 * n) + 1
by NAT_1:13;
then
d in (2 * n) + 1
by NAT_1:44;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by A17, A15, 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 A18:
c in (2 * n) \ 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 (2 * n) + 1
by NAT_1:44;
reconsider c =
c as
Nat by A18, NECKLACE:3;
c < 2
* n
by A18, Th2;
then
c < (2 * n) + 1
by NAT_1:13;
then
c in (2 * n) + 1
by NAT_1:44;
hence
z in [:((2 * n) + 1),((2 * n) + 1):]
by A22, A20, 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