defpred S₁[ Nat] means Mycielskian n is symmetric ;
P0: S₁[ 0 ] by Mycn1;
P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[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 A1: S₁[n] ; :: thesis: S₁[n + 1]
E1: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Mycn1;
set N = (3 * (2 |^ n)) -' 1;
F1: the carrier of (Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1 by E1, LNRS;
F1a: the carrier of (Mycielskian n) = (3 * (2 |^ n)) -' 1 by LNRS;
let x, y be set ; :: according to RELAT_2:def 3,NECKLACE:def 4 :: thesis: ( 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
H1: x in the carrier of (Mycielskian (n + 1)) and
I1: y in the carrier of (Mycielskian (n + 1)) and
J1: [x,y] in the InternalRel of (Mycielskian (n + 1)) ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
reconsider xp1 = x, yp1 = y as Nat by F1, H1, I1, NECKLACE:4;
L1: [xp1,yp1] in the InternalRel of (Mycielskian (n + 1)) by J1;

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 L1, E1, iMR0;

suppose ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))

then ( xp1 in (3 * (2 |^ n)) -' 1 & yp1 in (3 * (2 |^ n)) -' 1 ) by NAT_1:45;
then A2: [yp1,xp1] in the InternalRel of (Mycielskian n) by A1, F1a, Sym0a, J1, E1, iMR1b;
the InternalRel of (Mycielskian n) c= the InternalRel of (Mycielskian (n + 1)) by E1, iMR1ba;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A2; :: thesis: verum

end;

suppose that S1: xp1 < (3 * (2 |^ n)) -' 1 and
S2: (3 * (2 |^ n)) -' 1 <= yp1 and
S3: yp1 < 2 * ((3 * (2 |^ n)) -' 1) ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))

consider yy being Nat such that
A2: yp1 = ((3 * (2 |^ n)) -' 1) + yy by S2, NAT_1:10;
B2: xp1 in (3 * (2 |^ n)) -' 1 by S1, NAT_1:45;
yy + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by S3, A2;
then yy < (3 * (2 |^ n)) -' 1 by XREAL_1:8;
then C2: yy in (3 * (2 |^ n)) -' 1 by NAT_1:45;
[x,yy] in the InternalRel of (Mycielskian n) by J1, B2, A2, E1, iMR1c;
then [yy,x] in the InternalRel of (Mycielskian n) by C2, B2, F1a, A1, Sym0a;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by E1, L1, A2, iMR1a; :: thesis: verum

end;

suppose that S1: (3 * (2 |^ n)) -' 1 <= xp1 and
S2: xp1 < 2 * ((3 * (2 |^ n)) -' 1) and
S3: yp1 < (3 * (2 |^ n)) -' 1 ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))

consider xx being Nat such that
A2: xp1 = ((3 * (2 |^ n)) -' 1) + xx by S1, NAT_1:10;
B2: yp1 in (3 * (2 |^ n)) -' 1 by S3, NAT_1:45;
xx + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by A2, S2;
then xx < (3 * (2 |^ n)) -' 1 by XREAL_1:8;
then C2: xx in (3 * (2 |^ n)) -' 1 by NAT_1:45;
[xx,y] in the InternalRel of (Mycielskian n) by B2, J1, E1, A2, iMR1d;
then [y,xx] in the InternalRel of (Mycielskian n) by C2, B2, F1a, A1, Sym0a;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by E1, L1, A2, iMR1a; :: thesis: verum

end;

suppose ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))

hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by E1, iMR1e; :: thesis: verum

end;

suppose ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) ; :: thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))

hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by E1, iMR1e; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P0, P1);
hence Mycielskian n is symmetric ; :: thesis: verum