defpred S2[ Nat] means Mycielskian n is symmetric ;
A1:
S2[ 0 ]
by Th49;
A2:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
set cMRn = the
carrier of
(Mycielskian n);
set iMRn = the
InternalRel of
(Mycielskian n);
set cMRn1 = the
carrier of
(Mycielskian (n + 1));
set iMRn1 = the
InternalRel of
(Mycielskian (n + 1));
assume A3:
S2[
n]
;
S2[n + 1]
A4:
Mycielskian (n + 1) = Mycielskian (Mycielskian n)
by Th49;
set N =
(3 * (2 |^ n)) -' 1;
A5:
the
carrier of
(Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1
by A4, Def7;
A6:
the
carrier of
(Mycielskian n) = (3 * (2 |^ n)) -' 1
by Def7;
let x,
y be
object ;
RELAT_2:def 3,
NECKLACE:def 3 ( not x in the carrier of (Mycielskian (n + 1)) or not y in the carrier of (Mycielskian (n + 1)) or not [x,y] in the InternalRel of (Mycielskian (n + 1)) or [y,x] in the InternalRel of (Mycielskian (n + 1)) )
assume that A7:
x in the
carrier of
(Mycielskian (n + 1))
and A8:
y in the
carrier of
(Mycielskian (n + 1))
and A9:
[x,y] in the
InternalRel of
(Mycielskian (n + 1))
;
[y,x] in the InternalRel of (Mycielskian (n + 1))
(
x in Segm ((2 * ((3 * (2 |^ n)) -' 1)) + 1) &
y in Segm ((2 * ((3 * (2 |^ n)) -' 1)) + 1) )
by A5, A7, A8;
then reconsider xp1 =
x,
yp1 =
y as
Nat ;
A10:
[xp1,yp1] in the
InternalRel of
(Mycielskian (n + 1))
by A9;
per cases
( ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 < (3 * (2 |^ n)) -' 1 & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) )
by A10, A4, Th38;
suppose that A12:
xp1 < (3 * (2 |^ n)) -' 1
and A13:
(3 * (2 |^ n)) -' 1
<= yp1
and A14:
yp1 < 2
* ((3 * (2 |^ n)) -' 1)
;
[y,x] in the InternalRel of (Mycielskian (n + 1))consider yy being
Nat such that A15:
yp1 = ((3 * (2 |^ n)) -' 1) + yy
by A13, NAT_1:10;
A16:
xp1 in Segm ((3 * (2 |^ n)) -' 1)
by A12, NAT_1:44;
yy + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1)
by A14, A15;
then
yy < (3 * (2 |^ n)) -' 1
by XREAL_1:6;
then A17:
yy in Segm ((3 * (2 |^ n)) -' 1)
by NAT_1:44;
[x,yy] in the
InternalRel of
(Mycielskian n)
by A9, A16, A15, A4, Th42;
then
[yy,x] in the
InternalRel of
(Mycielskian n)
by A17, A16, A6, A3, Th5;
hence
[y,x] in the
InternalRel of
(Mycielskian (n + 1))
by A4, A10, A15, Th41;
verum end; suppose that A18:
(3 * (2 |^ n)) -' 1
<= xp1
and A19:
xp1 < 2
* ((3 * (2 |^ n)) -' 1)
and A20:
yp1 < (3 * (2 |^ n)) -' 1
;
[y,x] in the InternalRel of (Mycielskian (n + 1))consider xx being
Nat such that A21:
xp1 = ((3 * (2 |^ n)) -' 1) + xx
by A18, NAT_1:10;
A22:
yp1 in Segm ((3 * (2 |^ n)) -' 1)
by A20, NAT_1:44;
xx + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1)
by A21, A19;
then
xx < (3 * (2 |^ n)) -' 1
by XREAL_1:6;
then A23:
xx in Segm ((3 * (2 |^ n)) -' 1)
by NAT_1:44;
[xx,y] in the
InternalRel of
(Mycielskian n)
by A22, A9, A4, A21, Th43;
then
[y,xx] in the
InternalRel of
(Mycielskian n)
by A23, A22, A6, A3, Th5;
hence
[y,x] in the
InternalRel of
(Mycielskian (n + 1))
by A4, A10, A21, Th41;
verum end;
end;
for n being Nat holds S2[n]
from NAT_1:sch 2(A1, A2);
hence
Mycielskian n is symmetric
; verum