The Mizar article:

The Class of Series -- Parallel Graphs. Part I

by
Krzysztof Retel

Received November 18, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: NECKLACE
[ MML identifier index ]


environ

 vocabulary ORDINAL2, ARYTM_3, NECKLACE, FUNCT_3, ARYTM, FUNCT_2, PARTFUN1,
      ORDERS_1, PRE_TOPC, RELAT_1, RELAT_2, REALSET1, FUNCT_1, BOOLE, SEQM_3,
      SUBSET_1, WELLORD1, CAT_1, FUNCOP_1, FUNCT_4, ARYTM_1, TARSKI, CARD_1,
      CARD_2, FINSET_1, SQUARE_1, INCPROJ;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_1, CARD_2,
      WELLORD1, FINSET_1, SQUARE_1, QUIN_1, REALSET1, ORDINAL1, NUMBERS,
      XCMPLX_0, XREAL_0, REAL_1, NAT_1, STRUCT_0, ORDERS_1, RELAT_1, RELAT_2,
      BINARITH, BVFUNC24, FUNCT_3, CQC_LANG, FUNCOP_1, RELSET_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FUNCT_4, ORDINAL2, WAYBEL_0, WAYBEL_1, ORDERS_3,
      PRE_TOPC;
 constructors ORDERS_3, QUIN_1, ENUMSET1, CARD_2, BVFUNC24, SQUARE_1, WELLORD1,
      WAYBEL_1, SEQM_3, REAL_1, BINARITH, AMISTD_1, MEMBERED, PRE_TOPC;
 clusters RELSET_1, ORDERS_1, STRUCT_0, SUBSET_1, ARYTM_3, XREAL_0, HILBERT3,
      TEX_2, FUNCT_1, FUNCT_4, FINSET_1, AFINSQ_1, SQUARE_1, ORDERS_3,
      TOPREAL8, FUNCOP_1, AMISTD_1, MEMBERED, FUNCT_2, NUMBERS, ORDINAL2;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
 definitions WAYBEL_0, WAYBEL_1, ORDERS_3, STRUCT_0, FUNCT_1, RELAT_1, RELAT_2,
      XBOOLE_0, TARSKI;
 theorems PRE_TOPC, FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, RELSET_1, ZFMISC_1,
      NAT_1, AXIOMS, CARD_1, ORDINAL2, STRUCT_0, WAYBEL_0, SUBSET_1, XBOOLE_0,
      XBOOLE_1, MCART_1, QUIN_1, WELLORD2, REAL_1, WELLORD1, RELAT_1, CQC_THE1,
      KNASTER, FUNCT_3, TARSKI, AMI_1, REALSET1, CQC_LANG, ORDERS_1, RELAT_2,
      FUNCOP_1, ORDINAL1, CARD_2, CARD_5, SQUARE_1, WAYBEL_1, BVFUNC24,
      ORDERS_3, SCMFSA_7, YELLOW11, CIRCCMB2, PARTFUN1, EULER_1, XCMPLX_0,
      XCMPLX_1;
 schemes NAT_1, FRAENKEL, FUNCT_7;

begin    :: Preliminaries

 reserve i,j,k,n for natural number;
 reserve x,x1,x2,x3,x4,x5,y1,y2,y3 for set;

definition let x1,x2,x3,x4,x5 be set;
  pred x1, x2, x3, x4, x5 are_mutually_different means :Def1:
  x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 &
  x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5;
end;

theorem
     x1,x2,x3,x4,x5 are_mutually_different
   implies card {x1,x2,x3,x4,x5} = 5
  proof
   assume x1,x2,x3,x4,x5 are_mutually_different;
   then x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 &
      x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 by Def1;
   then card {x1,x2,x3,x4} = 4 & not x5 in {x1,x2,x3,x4} &
      {x1,x2,x3,x4} is finite & {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
      by CARD_2:78,ENUMSET1:18,50;
   hence card {x1,x2,x3,x4,x5} = 4+1 by CARD_2:54 .= 5;
  end;

theorem Th2:
   4 = {0,1,2,3}
proof
  set x = {i where i is Nat: i < 4};
A1: x c= {0,1,2,3}
  proof
   let y be set;
   assume y in x;
   then consider i being Nat such that
A2: y=i & i < 3+1;
     i <= 3 by A2,NAT_1:38;
   then i = 0 or i=1 or i=2 or i=3 by CQC_THE1:4;
   hence y in {0,1,2,3} by A2,ENUMSET1:19;
  end;
A3: {0,1,2,3} c= x
    proof
     let y be set;
     assume y in {0,1,2,3};
     then y=0 or y=1 or y=2 or y=3 by ENUMSET1:18;
     hence y in x;
    end;
  thus 4 = x by AXIOMS:30
  .= {0,1,2,3} by A1,A3,XBOOLE_0:def 10;
end;

theorem
Th3:   [:{x1,x2,x3},{y1,y2,y3}:] =
   {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
  proof thus
     [:{x1,x2,x3},{y1,y2,y3}:] = [:{x1}\/{x2,x3}, {y1,y2,y3}:] by ENUMSET1:42
             .= [:{x1}\/{x2,x3}, {y1}\/ {y2,y3}:] by ENUMSET1:42
             .= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:]
                 \/ [:{x2,x3},{y1}:] \/ [:{x2,x3},{y2,y3}:] by ZFMISC_1:121
             .= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:]
                 \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:132
             .= {[x1,y1]} \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:]
                 \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:35
             .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ [:{x2,x3},{y1}:]
                 \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:36
             .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}
                 \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:36
             .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}
                 \/ ({[x2,y2],[x2,y3]} \/ [:{x3},{y2,y3}:]) by ZFMISC_1:36
             .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}
                 \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ZFMISC_1:36
             .= {[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}
                 \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:42
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]}
                 \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:49
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]}
                \/ {[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:45
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3],
                         [x3,y2],[x3,y3]} by BVFUNC24:31
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/
                {[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by BVFUNC24:30
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/
              ({[x3,y1],[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:49
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/
             ({[x2,y2],[x2,y3],[x3,y1]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:100
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/
                ({[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}) by ENUMSET1:49
             .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],
                       [x3,y1],[x3,y2],[x3,y3]} by BVFUNC24:30;
  end;

theorem Th4:
   for x being set, n be natural number holds
       x in n implies x is natural number
proof
  let x being set,n be natural number;
  assume
A1:  x in n;
  reconsider m=n as Nat by ORDINAL2:def 21;
    x in {j where j is Nat: j < m} by A1,AXIOMS:30;
  then ex j being Nat st x=j & j < m;
  hence thesis;
 end;

theorem Th5:
   for x be non empty natural number holds 0 in x
proof
 let x be non empty natural number;
 reconsider n = x as Nat by ORDINAL2:def 21;
A1:  n = {i where i is Nat: i < n} by AXIOMS:30;
    0 < n by NAT_1:19;
 hence thesis by A1;
end;

definition
 cluster natural -> cardinal set;
 coherence
  proof
   let X be set;
   assume X is natural;
   then X in omega by ORDINAL2:def 21;
   hence X is cardinal by CARD_1:65;
  end;
end;

definition
 let X be set;
 cluster delta X -> one-to-one;
 coherence
  proof
   let x1,x2 be set;
   set f = delta X;
   assume that A1:x1 in dom f and A2: x2 in dom f and A3: f.x1 = f.x2;
A4:  f.x1 = [x1,x1] by A1,FUNCT_3:def 7;
    f.x2 = [x2,x2] by A2,FUNCT_3:def 7;
  hence thesis by A3,A4,ZFMISC_1:33;
  end;
end;

theorem
Th6:   for X being set holds Card id X = Card X
 proof
  let X be set;
  id X in Funcs(X,X) by FUNCT_2:12;
  hence thesis by CARD_2:7;
 end;

definition let R be trivial Relation;
  cluster dom R -> trivial;
  coherence
  proof
  per cases by REALSET1:def 12;
  suppose R is empty;
  hence thesis by RELAT_1:60;
  suppose ex x being set st R = {x};
  then consider x being set such that
A1:  R = {x};
    x in R by A1,TARSKI:def 1;
  then consider y,z being set such that
A2:  x=[y,z] by RELAT_1:def 1;
    dom R = {y} by A1,A2,RELAT_1:23;
  hence thesis;
  end;
end;

definition
  cluster trivial -> one-to-one Function;
  coherence
  proof
  let f be Function such that
A1:  f is trivial;
  let x1,x2 be set;
  assume that
A2:  x1 in dom f & x2 in dom f and
    f.x1 = f.x2;
  reconsider f as trivial Function by A1;
  consider x being set such that
A3: dom f = {x} by A2,REALSET1:def 12;
    x1 = x & x2 = x by A2,A3,TARSKI:def 1;
  hence thesis;
  end;
end;

theorem
Th7:   for f,g be Function st dom f misses dom g holds
        rng(f +* g) = rng f \/ rng g
  proof
   let f,g be Function such that
A1:    dom f misses dom g;
      f tolerates g by A1,PARTFUN1:138;
    hence thesis by CIRCCMB2:5;
  end;

theorem
Th8:   for f,g be one-to-one Function st dom f misses dom g &
   rng f misses rng g holds (f+*g)" = f" +* g"
proof
 let f,g be one-to-one Function such that
A1:  dom f misses dom g and
A2:  rng f misses rng g;
A3:  dom (f" +* g") = dom (f") \/ dom (g") by FUNCT_4:def 1
                .= rng f \/ dom (g") by FUNCT_1:55
                .= rng f \/ rng g by FUNCT_1:55
                .= rng (f +* g) by A1,Th7;
A4: (f+*g) is one-to-one by A2,KNASTER:1;
    for y,x being set holds y in rng (f+*g) & x = (f" +* g").y
                     iff x in dom (f+*g) & y = (f+*g).x
  proof
   let y,x be set;
   thus y in rng (f+*g) & x = (f" +* g").y implies x in dom (f+*g) &
          y = (f+*g).x
    proof
     assume that
A5:  y in rng (f+*g) and
A6:  x = (f" +* g").y;
A7:     rng (f+*g) c= rng f \/ rng g by FUNCT_4:18;
     per cases by A5,A7,XBOOLE_0:def 2;
     suppose A8: y in rng f;
     then consider z being set such that
A9:     z in dom f and
A10:     y = f.z by FUNCT_1:def 5;
       dom (f +* g) = dom f \/ dom g by FUNCT_4:def 1;
     then A11:z in dom (f +* g) by A9,XBOOLE_0:def 2;
A12:     y = (f +* g).z by A1,A9,A10,FUNCT_4:17;
     A13: z = f".y by A9,A10,FUNCT_1:54;
       dom (f") = rng f & dom (g") = rng g by FUNCT_1:55;
     hence thesis by A2,A6,A8,A11,A12,A13,FUNCT_4:17;
     suppose A14: y in rng g;
     then consider z being set such that
A15:     z in dom g and
A16:     y = g.z by FUNCT_1:def 5;
A17:     dom (f +* g) = dom f \/ dom g by FUNCT_4:def 1;
A18:  y = (g +* f).z by A1,A15,A16,FUNCT_4:17;
     A19: z = g".y by A15,A16,FUNCT_1:54;
     A20: dom (f") = rng f & dom (g") = rng g by FUNCT_1:55;
     then z = (g" +* f").y by A2,A14,A19,FUNCT_4:17;
     then z = x by A2,A6,A20,FUNCT_4:36;
     hence thesis by A1,A15,A17,A18,FUNCT_4:36,XBOOLE_0:def 2;
    end;
   thus x in dom (f+*g) & y = (f+*g).x implies y in rng (f+*g) &
          x = (f" +* g").y
    proof
     assume that
A21:   x in dom (f+*g) and
A22:   y = (f+*g).x;
A23:    dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
     per cases by A21,A23,XBOOLE_0:def 2;
     suppose A24: x in dom f;
then not x in dom g by A1,XBOOLE_0:3;
then A25:    y = f.x by A22,FUNCT_4:12;
      then A26:y in rng f by A24,FUNCT_1:def 5;
      then A27: y in rng f \/ rng g by XBOOLE_0:def 2;
      A28:x = f".y by A24,A25,FUNCT_1:54;
        dom (f") = rng f & dom (g") = rng g by FUNCT_1:55;
     hence thesis by A1,A2,A26,A27,A28,Th7,FUNCT_4:17;
     suppose A29:x in dom g;
then A30:    y = g.x by A22,FUNCT_4:14;
      then A31:y in rng g by A29,FUNCT_1:def 5;
      then A32:y in rng f \/ rng g by XBOOLE_0:def 2;
      A33: x = g".y by A29,A30,FUNCT_1:54;
      A34: dom (f") = rng f & dom (g") = rng g by FUNCT_1:55;
      then x = (g" +* f").y by A2,A31,A33,FUNCT_4:17;
     hence thesis by A1,A2,A32,A34,Th7,FUNCT_4:36;
    end;
  end;
  hence thesis by A3,A4,FUNCT_1:54;
end;

theorem
    for A,a,b being set holds (A --> a) +* (A --> b) = A --> b
proof
 let A,a,b be set;
 set g = A --> b;
  dom g = A by FUNCOP_1:19;
    then dom (A --> a) c= dom g by FUNCOP_1:19;
 hence thesis by FUNCT_4:20;
end;

theorem
Th10:  for a,b being set holds (a .--> b)" = b .--> a
 proof
  let a,b be set;
  set f = a .--> b,
      g = b .--> a;
A1:  dom g = {b} by CQC_LANG:5
          .= rng f by CQC_LANG:5;
    for y,x be set holds y in rng f & x = g.y iff x in dom f & y = f.x
  proof
   let y,x be set;
   thus y in rng f & x = g.y implies x in dom f & y = f.x
     proof
     assume that
A2:   y in rng f and
A3:   x = g.y;
A4:     y in {b} by A2,CQC_LANG:5;
     then A5: x = g.b by A3,TARSKI:def 1
               .= a by CQC_LANG:6;
     then A6:x in {a} by TARSKI:def 1;
       f.x = b by A5,CQC_LANG:6
        .= y by A4,TARSKI:def 1;
     hence thesis by A6,CQC_LANG:5;
     end;
     assume that
A7:   x in dom f and
A8:    y = f.x;
A9:     x in {a} by A7,CQC_LANG:5;
     then A10: y = f.a by A8,TARSKI:def 1
               .= b by CQC_LANG:6;
     then A11:y in {b} by TARSKI:def 1;
       g.y = a by A10,CQC_LANG:6
        .= x by A9,TARSKI:def 1;
     hence thesis by A11,CQC_LANG:5;
  end;
  hence thesis by A1,FUNCT_1:54;
 end;

theorem
Th11:  for a,b,c,d being set st a = b iff c = d
       holds (a,b) --> (c,d)" = (c,d) --> (a,b)
 proof
 let a,b,c,d being set such that A1:a = b iff c = d;
 per cases by A1;
  suppose A2: a = b & c = d;
    (a,a) --> (d,d)" = (a .--> d)" by AMI_1:20
                  .= (d .--> a) by Th10
                  .= (d,d) --> (a,a) by AMI_1:20;
  hence thesis by A2;
  suppose A3:a <> b & c <> d;
  set f = (a,b) --> (c,d),
      g = (c,d) --> (a,b);
A4: f is one-to-one
    proof
     let x1,x2 being set such that
A5:  x1 in dom f & x2 in dom f and
A6:  f.x1 = f.x2;
A7:     dom f = {a,b} by FUNCT_4:65;
     per cases by A5,A7,TARSKI:def 2;
      suppose x1 = a & x2 = a or x1 = b & x2 = b;
      hence thesis;
      suppose x1 = a & x2 = b;
      then f.x1 = c & f.x2 = d by A3,FUNCT_4:66;
      hence thesis by A3,A6;
      suppose x1 = b & x2 = a;
      then f.x1 = d & f.x2 = c by A3,FUNCT_4:66;
      hence thesis by A3,A6;
     thus thesis;
    end;
A8: dom g = {c,d} by FUNCT_4:65
        .= rng f by A3,FUNCT_4:67;
    for y,x be set holds y in rng f & x = g.y iff x in dom f & y = f.x
  proof
   let y,x be set;
A9:   y in rng f & x = g.y implies x in dom f & y = f.x
    proof
    assume that
A10:   y in rng f and
A11:   x = g.y;
A12:    y in {c,d} by A3,A10,FUNCT_4:67;
    per cases by A12,TARSKI:def 2;
    suppose A13: y = c;
    then A14: x = a by A3,A11,FUNCT_4:66;
    then x in {a,b} by TARSKI:def 2;
    hence thesis by A3,A13,A14,FUNCT_4:65,66;
    suppose A15: y = d;
    then A16: x = b by A3,A11,FUNCT_4:66;
    then x in {a,b} by TARSKI:def 2;
    hence thesis by A3,A15,A16,FUNCT_4:65,66;
    end;
      x in dom f & y = f.x implies y in rng f & x = g.y
    proof
    assume that
A17:  x in dom f and
A18:  y = f.x;
A19:   x in {a,b} by A17,FUNCT_4:65;
    per cases by A19,TARSKI:def 2;
    suppose A20: x = a;
    then A21: y = c by A3,A18,FUNCT_4:66;
    then y in {c,d} by TARSKI:def 2;
    hence thesis by A3,A20,A21,FUNCT_4:66,67;
    suppose A22: x = b;
    then A23: y = d by A3,A18,FUNCT_4:66;
    then y in {c,d} by TARSKI:def 2;
    hence thesis by A3,A22,A23,FUNCT_4:66,67;
    end;
   hence thesis by A9;
  end;
  hence thesis by A4,A8,FUNCT_1:54;
 end;

scheme Convers{X()-> non empty set, R() -> Relation, F,G(set)-> set, P[set]}:
 R()~ ={[F(x),G(x)] where x is Element of X(): P[x]}
 provided
A1:  R() = {[G(x),F(x)] where x is Element of X(): P[x]}
proof
 set S = {[F(x),G(x)] where x is Element of X(): P[x]};
   S is Relation-like
 proof
  let x being set;
  assume x in S;
  then ex y being Element of X() st x = [F(y),G(y)] & P[y];
  hence thesis;
 end;
 then reconsider S' = S as Relation;
    for x,y being set holds [x,y] in S' iff [y,x] in R()
  proof
A2:   for x,y being set holds [x,y] in S' implies [y,x] in R()
   proof
    let x,y being set;
    assume [x,y] in S';
    then consider z being Element of X() such that
A3:   [x,y] = [F(z),G(z)] and
A4:   P[z];
     x = F(z) & y = G(z) by A3,ZFMISC_1:33;
    hence thesis by A1,A4;
   end;
     for x,y being set holds [y,x] in R() implies [x,y] in S'
   proof
    let x,y being set;
    assume [y,x] in R();
    then consider z being Element of X() such that
A5:   [y,x] = [G(z),F(z)] and
A6:   P[z] by A1;
     y = G(z) & x = F(z) by A5,ZFMISC_1:33;
    hence thesis by A6;
   end;
   hence thesis by A2;
  end;
 hence S = R()~ by RELAT_1:def 7;
end;

theorem
     for i,j,n be natural number holds
   i < j & j in n implies i in n
   proof
     let i,j,n be natural number;
     assume
A1:   i < j & j in n;
     then j < n by EULER_1:1;
     then i < n by A1,AXIOMS:22;
     hence thesis by EULER_1:1;
   end;

begin   :: Auxiliary Concepts

definition let R,S be RelStr;
  pred S embeds R means
:Def2:  ex f being map of R,S st f is one-to-one
  & for x,y being Element of R holds
  [x,y] in the InternalRel of R iff [f.x,f.y] in the InternalRel of S;
end;

definition let R,S be non empty RelStr;
  redefine pred S embeds R;
 reflexivity
  proof let R be non empty RelStr;
    set f = id the carrier of R;
    reconsider f as map of R,R;
   take f;
   thus f is one-to-one by FUNCT_1:52;
   let x,y be Element of R;
      x = f.x & y = f.y by FUNCT_1:35;
    hence thesis;
  end;
end;

theorem
Th13:   for R,S,T be non empty RelStr holds
   R embeds S & S embeds T implies R embeds T
 proof
  let R,S,T be non empty RelStr;
  assume R embeds S;
  then consider f being map of S,R such that
A1: f is one-to-one and
A2: for x,y being Element of S holds
  [x,y] in the InternalRel of S iff [f.x,f.y] in the InternalRel of R by Def2;
  assume S embeds T;
  then consider g being map of T,S such that
A3: g is one-to-one and
A4: for x,y being Element of T holds
  [x,y] in the InternalRel of T iff [g.x,g.y] in the InternalRel of S by Def2;
   reconsider h=f*g as map of T,R;
   take h;
   thus h is one-to-one by A1,A3,FUNCT_1:46;
   thus for x,y being Element of T holds
   [x,y] in the InternalRel of T
   iff [h.x,h.y] in the InternalRel of R
   proof
    let x,y be Element of T;
    thus [x,y] in the InternalRel of T
    implies [h.x,h.y] in the InternalRel of R
      proof
       assume [x,y] in the InternalRel of T;
       then A5:[g.x,g.y] in the InternalRel of S by A4;
        h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:21;
       hence thesis by A2,A5;
      end;
    thus [h.x,h.y] in the InternalRel of R
    implies [x,y] in the InternalRel of T
      proof
       assume A6:[h.x,h.y] in the InternalRel of R;
         h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:21;
       then [g.x,g.y] in the InternalRel of S by A2,A6;
       hence thesis by A4;
      end;
   end;
 end;

definition let R,S be non empty RelStr;
 pred R is_equimorphic_to S means
:Def3: R embeds S & S embeds R;
 reflexivity;
 symmetry;
end;

theorem
     for R,S,T be non empty RelStr holds
   R is_equimorphic_to S & S is_equimorphic_to T implies
   R is_equimorphic_to T
 proof
   let R,S,T be non empty RelStr;
   assume R is_equimorphic_to S & S is_equimorphic_to T;
   then R embeds S & S embeds R & S embeds T & T embeds S by Def3;
   then R embeds T & T embeds R by Th13;
   hence thesis by Def3;
 end;

definition
  let R be non empty RelStr;
  redefine attr R is connected;
  antonym R is parallel;
end;

definition let R be RelStr;
 attr R is symmetric means
:Def4: the InternalRel of R is_symmetric_in the carrier of R;
end;

definition let R be RelStr;
 attr R is asymmetric means
:Def5: the InternalRel of R is asymmetric;
end;

theorem
     for R be RelStr st R is asymmetric holds
   the InternalRel of R misses (the InternalRel of R)~
  proof
   let R be RelStr such that
A1:     R is asymmetric;
   assume the InternalRel of R meets (the InternalRel of R)~;
   then consider x being set such that
A2:   x in the InternalRel of R and
A3:   x in (the InternalRel of R)~ by XBOOLE_0:3;
   consider y,z being set such that
A4:      x = [y,z] by A3,RELAT_1:def 1;
A5:   [z,y] in the InternalRel of R by A3,A4,RELAT_1:def 7;
     the InternalRel of R is asymmetric by A1,Def5;
   then A6:   the InternalRel of R is_asymmetric_in field
            (the InternalRel of R) by RELAT_2:def 13;
     y in field the InternalRel of R &
   z in field the InternalRel of R by A2,A4,RELAT_1:30;
   hence contradiction by A2,A4,A5,A6,RELAT_2:def 5;
  end;

definition let R be RelStr;
 attr R is irreflexive means
   for x being set st x in the carrier of R
 holds not [x,x] in the InternalRel of R;
end;

definition
 let n be natural number;
 func n-SuccRelStr -> strict RelStr means
:Def7: the carrier of it = n &
 the InternalRel of it = {[i,i+1] where i is Nat:i+1 < n};
  existence
   proof
    set r = {[i,i+1] where i is Nat:i+1 < n};
      r c= [:n,n:]
     proof
      let x be set;
      assume x in r;
      then consider i be Nat such that
A1:   x = [i,i+1] and
A2:   i+1 < n;
        i <= i+1 by NAT_1:29;
      then i < n by A2,AXIOMS:22;
      then i in n & i+1 in n by A2,EULER_1:1;
      hence x in [:n,n:] by A1,ZFMISC_1:106;
     end;
    then reconsider r as Relation of n by RELSET_1:def 1;
    take RelStr (#n,r#);
    thus thesis;
   end;
  uniqueness;
end;

theorem
     for n be natural number holds n-SuccRelStr is asymmetric
  proof
   let n be natural number;
   set S = n-SuccRelStr;
   thus the InternalRel of S is asymmetric
    proof
     thus the InternalRel of S is_asymmetric_in field the InternalRel of S
     proof
      let x,y be set;
      assume that
          x in field the InternalRel of S &
        y in field the InternalRel of S and
A1:     [x,y] in the InternalRel of S;
        [x,y] in {[i,i+1] where i is Nat:i+1 < n} by A1,Def7;
      then consider i be Nat such that
A2:               [x,y] = [i,i+1] & i+1<n;
A3:       x = i & y = i+1 by A2,ZFMISC_1:33;
       assume [y,x] in the InternalRel of S;
       then [y,x] in {[i',i'+1] where i' is Nat:i'+1 < n} by Def7;
       then consider j be Nat such that
A4:       [y,x] = [j,j+1] & j+1<n;
        y = j & x = j+1 by A4,ZFMISC_1:33;
      then i+1+1 < i+1 by A3,NAT_1:38;
      hence contradiction by NAT_1:29;
     end;
    end;
  end;

theorem
Th17:   n > 0 implies Card the InternalRel of n-SuccRelStr = n-1
 proof
  assume
A1: n > 0;
then A2:    n >= 0+1 by NAT_1:38;
A3:   i in n-'1 implies i+1<n
     proof
      assume i in n-'1;
      then A4:i < n-'1 by EULER_1:1;
        n >= 0+1 by A1,NAT_1:38;
      then i < n-1 by A4,SCMFSA_7:3;
     hence thesis by REAL_1:86;
     end;
    deffunc F(Nat) = [$1,$1+1];
    defpred P[Nat] means $1+1<n;
    defpred Q[set] means $1 in n-'1;
A5: for i being Nat holds P[i] iff Q[i] proof
    let i be Nat;
    thus i+1<n implies i in n-'1
     proof
      assume i+1<n;
      then i < n-1 by REAL_1:86;
      then i < n-'1 by A2,SCMFSA_7:3;
      hence thesis by EULER_1:1;
     end;
    thus thesis by A3;
   end;
A6: {F(i) where i is Nat: P[i]} = {F(i) where i is Nat: Q[i]}
    from Fraenkel6'(A5);
A7: n-'1 c= NAT by ORDINAL1:def 2;
    deffunc F(Nat) = [$1,$1+1];
A8: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1 = d2
     by ZFMISC_1:33;
A9: n-'1, {F(i) where i is Nat: i in n-'1} are_equipotent
                from CardMono'(A7,A8);
  thus Card the InternalRel of n-SuccRelStr
           = Card {[i,i+1] where i is Nat:i+1 < n} by Def7
          .= Card (n-'1) by A6,A9,CARD_1:21
          .= n-'1 by CARD_1:66
          .= n-1 by A2,SCMFSA_7:3;
 end;

definition let R be RelStr;
 func SymRelStr R -> strict RelStr means
:Def8: the carrier of it = the carrier of R &
 the InternalRel of it = (the InternalRel of R) \/ (the InternalRel of R)~;
 existence
   proof
    take RelStr (#the carrier of R, (the InternalRel of R)
      \/ (the InternalRel of R)~ #);
    thus thesis;
   end;
 uniqueness;
end;

definition let R be RelStr;
 cluster SymRelStr R -> symmetric;
 coherence
  proof
   let x,y be set;
   assume that x in the carrier of SymRelStr R &
                   y in the carrier of SymRelStr R and
               A1: [x,y] in the InternalRel of SymRelStr R;
A2:  [x,y] in (the InternalRel of R) \/ (the InternalRel of R)~ by A1,Def8;
  per cases by A2,XBOOLE_0:def 2;
  suppose [x,y] in the InternalRel of R;
   then [y,x] in (the InternalRel of R)~ by RELAT_1:def 7;
   then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~
                      by XBOOLE_0:def 2;
  hence thesis by Def8;
  suppose [x,y] in (the InternalRel of R)~;
   then [y,x] in the InternalRel of R by RELAT_1:def 7;
   then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~
                      by XBOOLE_0:def 2;
  hence thesis by Def8;
  thus thesis;
  end;
end;

definition
 cluster non empty symmetric RelStr;
 existence
  proof
   set R = {[0,0]};
     R c= [:{0},{0}:] by ZFMISC_1:35;
   then reconsider R = {[0,0]} as Relation of {0} by RELSET_1:def 1;
   take S = RelStr (#{0},R#);
   thus S is non empty;
   thus the InternalRel of S is_symmetric_in the carrier of S
    proof
     let x,y be set;
     assume that x in the carrier of S &
                     y in the carrier of S and
                 A1: [x,y] in the InternalRel of S;
       x = 0 & y = 0 by A1,ZFMISC_1:34;
     then [y,x] in [:{0},{0}:] by ZFMISC_1:34;
     hence [y,x] in the InternalRel of S by ZFMISC_1:35;
    end;
  end;
end;

definition let R be symmetric RelStr;
 cluster the InternalRel of R -> symmetric;
 coherence
 proof
  let x,y be set;
  assume that A1: x in field the InternalRel of R &
                  y in field the InternalRel of R and
              A2: [x,y] in the InternalRel of R;
A3:  the InternalRel of R is_symmetric_in the carrier of R by Def4;
    field the InternalRel of R c= (the carrier of R) \/ the carrier of R
        by RELSET_1:19;
  hence thesis by A1,A2,A3,RELAT_2:def 3;
 end;
end;

Lm1: for S,R being non empty RelStr holds
      S,R are_isomorphic implies
          Card (the InternalRel of S) = Card (the InternalRel of R)
 proof
  let S,R being non empty RelStr;
  set A = the carrier of S,
      B = the carrier of R,
      C = the InternalRel of S,
      D = the InternalRel of R;
  reconsider C as set;
  assume S,R are_isomorphic;
  then consider f being map of S,R such that
A1:  f is isomorphic by WAYBEL_1:def 8;
A2:  f is monotone by A1,WAYBEL_0:def 38;
     reconsider f'=f as one-to-one Function by A1,WAYBEL_0:def 38;
A3:  [:f',f':] is one-to-one;
  A4: dom f = A by FUNCT_2:def 1;
A5:  rng f = B by A1,WAYBEL_0:66;
    the InternalRel of S,the InternalRel of R are_equipotent
  proof
   set F = [:f,f:]|C;
   set L = dom F;
   set P = [:f,f:];
A6:  dom F = dom ([:f,f:]) /\ C by FUNCT_1:68
                    .= [:dom f, dom f:] /\ C by FUNCT_3:def 9
                    .= C by A4,XBOOLE_1:28;
A7:   rng F c= D
       proof
        let a be set;
        assume a in rng F;
        then consider x being set such that
   A8:  x in dom F and
   A9:  a = F.x by FUNCT_1:def 5;
        consider x1,x2 being set such that
A10:     x = [x1,x2] by A8,RELAT_1:def 1;
A11:     x1 in dom f & x2 in dom f by A4,A8,A10,ZFMISC_1:106;
          a = P.x by A8,A9,FUNCT_1:70;
then A12:     a = [f.x1,f.x2] by A10,A11,FUNCT_3:def 9;
        reconsider X1 = x1, X2 = x2 as Element of S by A11;
          X1 <= X2 by A6,A8,A10,ORDERS_1:def 9;
        then f.X1 <= f.X2 by A2,ORDERS_3:def 5;
        hence thesis by A12,ORDERS_1:def 9;
       end;
   then rng F c= [:B,B:] by XBOOLE_1:1;
   then reconsider F as Function of L,[:B,B:] by FUNCT_2:4;
   reconsider F as Function of L,D by A7,FUNCT_2:8;
    A13:  F is one-to-one by A3,FUNCT_1:84;
  rng F = D
     proof
      thus rng F c= D by A7;
      let x be set;
      assume A14:x in D;
      then consider x1,x2 being set such that
A15:   x = [x1,x2] by RELAT_1:def 1;
A16:   x1 in B & x2 in B by A14,A15,ZFMISC_1:106;
      reconsider x1' = x1, x2' = x2 as Element of B by A14,A15,ZFMISC_1:106;
A17:      x1' <= x2' by A14,A15,ORDERS_1:def 9;
      consider X1 being set such that
A18:    X1 in dom f and
A19:    x1 = f.X1 by A5,A16,FUNCT_1:def 5;
     consider X2 being set such that
A20:   X2 in dom f and
A21:   x2 = f.X2 by A5,A16,FUNCT_1:def 5;
      reconsider X1' = X1, X2' = X2 as Element of S by A18,A20;
        X1' <= X2' by A1,A17,A19,A21,WAYBEL_0:66;
then A22:     [X1,X2] in C by ORDERS_1:def 9;
      set Pi = [X1,X2];
       Pi in [:dom f,dom f:] by A18,A20,ZFMISC_1:106;
      then x = [:f,f:].[X1,X2] by A15,A19,A21,FUNCT_3:86
        .= F.[X1,X2] by A6,A22,FUNCT_1:70;
      hence thesis by A6,A22,FUNCT_1:def 5;
     end;
     hence thesis by A6,A13,WELLORD2:def 4;
   end;
  hence thesis by CARD_1:21;
 end;

definition let R be RelStr;
  func ComplRelStr R -> strict RelStr means
:Def9:  the carrier of it = the carrier of R &
  the InternalRel of it = (the InternalRel of R)` \
   id (the carrier of R);
  existence
   proof
    reconsider r = (the InternalRel of R)` \ id (the carrier of R)
    as Relation of the carrier of R by RELSET_1:def 1;
    take RelStr(#the carrier of R, r#);
   thus thesis;
   end;
  uniqueness;
end;

definition let R be non empty RelStr;
 cluster ComplRelStr R -> non empty;
 coherence
  proof
     the carrier of ComplRelStr R = the carrier of R by Def9;
   hence the carrier of ComplRelStr R is non empty;
  end;
end;

theorem
Th18:   for S,R being RelStr holds
   S,R are_isomorphic implies
   Card the InternalRel of S = Card the InternalRel of R
proof
  let S,R be RelStr;
  assume A1: S,R are_isomorphic;
  then consider f being map of S,R such that
A2:  f is isomorphic by WAYBEL_1:def 8;
  per cases by A2,WAYBEL_0:def 38;
  suppose S is non empty & R is non empty;
  hence thesis by A1,Lm1;
  suppose S is empty & R is empty;
  then reconsider S, R as empty RelStr;
    the InternalRel of S = {} & the InternalRel of R = {};
  hence thesis;
end;

begin   :: Necklace n

definition let n be natural number;
 func Necklace n -> strict RelStr equals
:Def10: SymRelStr(n-SuccRelStr);
 coherence;
end;

definition let n be natural number;
 cluster Necklace n -> symmetric;
 coherence
 proof
    Necklace n = SymRelStr(n-SuccRelStr) by Def10;
  hence thesis;
 end;
end;

theorem
Th19:   the InternalRel of Necklace n
   = {[i,i+1] where i is Nat:i+1 < n} \/ {[i+1,i] where i is Nat:i+1 < n}
 proof
 set A = Necklace n;
 set B = n-SuccRelStr;
A1: A = SymRelStr B by Def10;
 set I = {[i,i+1] where i is Nat:i+1 < n};
     deffunc F(Nat) = $1;
    deffunc G(Nat) = $1+1;
    defpred P[Nat] means $1+1 < n;
 set R = {[G(i),F(i)] where i is Nat: P[i]};
   I is Relation-like
  proof
  let x be set;
  assume x in I;
  then ex i being Nat st x = [i,i+1] & i+1<n;
  hence thesis;
  end;
 then reconsider I as Relation;
A2: I = {[F(i),G(i)] where i is Nat: P[i]};
A3: I~ = R from Convers(A2);
   the InternalRel of B = I by Def7;
 hence the InternalRel of A
    = {[i,i+1] where i is Nat:i+1 < n} \/ R by A1,A3,Def8;
 end;

theorem
Th20:   for x be set holds x in the InternalRel of Necklace n iff
           ex i being Nat st i+1 < n & (x = [i,i+1] or x = [i+1,i])
 proof
  let x be set;
  thus x in the InternalRel of Necklace n implies
       ex i being Nat st i+1< n & (x = [i,i+1] or x = [i+1,i])
   proof
   assume that
A1:   x in the InternalRel of Necklace n;
     x in ({[i,i+1] where i is Nat:i+1 < n} \/ {[i+1,i] where i is Nat:i+1 < n}
)
          by A1,Th19;
   then x in {[i,i+1] where i is Nat:i+1 < n} or
        x in {[i+1,i] where i is Nat:i+1 < n} by XBOOLE_0:def 2;
   then (ex i being Nat st x = [i,i+1] & i+1<n) or
        (ex i being Nat st x = [i+1,i] & i+1<n);
   hence thesis;
   end;
  thus (ex i being Nat st i+1 < n & (x = [i,i+1] or x = [i+1,i])) implies
         x in the InternalRel of Necklace n
   proof
    given i being Nat such that
A2:  i+1 < n & (x=[i,i+1] or x=[i+1,i]);
    per cases by A2;
    suppose i+1 < n & x=[i,i+1];
     then x in {[j,j+1] where j is Nat:j+1 < n};
     then x in ({[j,j+1] where j is Nat:j+1 < n} \/
               {[j+1,j] where j is Nat:j+1 < n}) by XBOOLE_0:def 2;
    hence thesis by Th19;
    suppose i+1 < n & x=[i+1,i];
     then x in {[j+1,j] where j is Nat:j+1 < n};
     then x in ({[j+1,j] where j is Nat:j+1 < n} \/
               {[j,j+1] where j is Nat:j+1 < n}) by XBOOLE_0:def 2;
    hence thesis by Th19;
   end;
 end;

definition let n be natural number;
  cluster Necklace n -> irreflexive;
  coherence
  proof
  set A = Necklace n;
  let x be set;
  assume x in the carrier of A;
  assume A1:[x,x] in the InternalRel of A;
A2:  the InternalRel of Necklace n
    = {[i,i+1] where i is Nat:i+1 < n} \/ {[i+1,i] where i is Nat:i+1 < n}
      by Th19;
  per cases by A1,A2,XBOOLE_0:def 2;
   suppose [x,x] in {[i,i+1] where i is Nat:i+1 < n};
   then consider i being Nat such that
A3:   [x,x] = [i,i+1] & i+1 < n;
     x = i & x = i+1 by A3,ZFMISC_1:33;
   hence contradiction by REAL_1:69;
   suppose [x,x] in {[i+1,i] where i is Nat:i+1 < n};
   then consider i being Nat such that
A4:   [x,x] = [i+1,i] & i+1 < n;
     x = i+1 & x = i by A4,ZFMISC_1:33;
   hence contradiction by REAL_1:69;
  end;
end;

theorem
Th21:   for n be natural number holds the carrier of Necklace n = n
  proof
    let n be natural number;
      the carrier of Necklace n =
    the carrier of SymRelStr(n-SuccRelStr) by Def10
    .= the carrier of n-SuccRelStr by Def8
    .= n by Def7;
    hence thesis;
  end;

definition let n be non empty natural number;
  cluster Necklace n -> non empty;
   coherence
   proof
      the carrier of Necklace n = n by Th21;
    hence thesis by STRUCT_0:def 1;
   end;
end;

definition let n be natural number;
  cluster the carrier of Necklace n -> finite;
  coherence by Th21;
end;

theorem Th22:
   for n,i be natural number st i+1 < n holds
   [i,i+1] in the InternalRel of Necklace n
proof
  let n,j be natural number such that
A1:  j+1 < n;
A2:  the InternalRel of Necklace n
      = {[i,i+1] where i is Nat:i+1 < n} \/ {[i+1,i] where i is Nat:i+1 < n}
          by Th19;
  reconsider j as Nat by ORDINAL2:def 21;
    [j,j+1] in {[i,i+1] where i is Nat:i+1 < n} by A1;
  hence thesis by A2,XBOOLE_0:def 2;
end;

theorem Th23:
   for n be natural number, i being natural number
   st i in the carrier of Necklace n holds i < n
proof
  let n be natural number, i being natural number such that
A1:    i in the carrier of Necklace n;
    i in n by A1,Th21;
  hence thesis by EULER_1:1;
end;

theorem
     for n be non empty natural number holds Necklace n is connected
  proof
   let n be non empty natural number;
   given X,Y being Subset of Necklace n such that
A1: X <> {} and
A2:  Y <> {} and
A3: [#] Necklace n = X \/ Y and
A4: X misses Y and
A5: the InternalRel of Necklace n =
     (the InternalRel of Necklace n)|_2 X \/
      (the InternalRel of Necklace n) |_2 Y;
A6:   the carrier of Necklace n = X \/ Y by A3,PRE_TOPC:def 3;
A7:   the carrier of Necklace n = n by Th21;
A8:   0 in n by Th5;
   per cases by A6,A7,A8,XBOOLE_0:def 2;
   suppose
A9:   0 in X;
   defpred P[natural number] means $1 in Y;
   consider x being Element of Necklace n such that
A10: x in Y by A2,SUBSET_1:10;
     x in the carrier of Necklace n;
   then x in n by Th21;
   then x is natural by Th4;
   then x is Nat by ORDINAL2:def 21;
   then A11: ex x being Nat st P[x] by A10;
   consider k being Nat such that
A12:  P[k] and
A13:  for i being Nat st P[i] holds k <= i from Min (A11);
     k <> 0 by A4,A9,A12,XBOOLE_0:3;
   then consider i being Nat such that
A14:  k = i+1 by NAT_1:22;
     i < i+1 by REAL_1:69;
   then A15:   not i in Y by A13,A14;
A16: not i+1 in X by A4,A12,A14,XBOOLE_0:3;
     i+1 < n by A12,A14,Th23;
   then A17:  [i,i+1] in the InternalRel of Necklace n by Th22;
     now per cases by A5,A17,XBOOLE_0:def 2;
    suppose [i,i+1] in (the InternalRel of Necklace n) |_2 X;
     then [i,i+1] in [:X,X:] by WELLORD1:16;
    hence contradiction by A16,ZFMISC_1:106;
    suppose [i,i+1] in (the InternalRel of Necklace n) |_2 Y;
     then [i,i+1] in [:Y,Y:] by WELLORD1:16;
    hence contradiction by A15,ZFMISC_1:106;
   end;
   hence contradiction;
   suppose
A18:   0 in Y;
   defpred P[natural number] means $1 in X;
   consider y being Element of Necklace n such that
A19: y in X by A1,SUBSET_1:10;
     y in the carrier of Necklace n;
   then y in n by Th21;
   then y is natural by Th4;
   then y is Nat by ORDINAL2:def 21;
   then A20: ex y being Nat st P[y] by A19;
   consider k being Nat such that
A21:  P[k] and
A22:  for i being Nat st P[i] holds k <= i from Min (A20);
     k <> 0 by A4,A18,A21,XBOOLE_0:3;
   then consider i being Nat such that
A23:  k = i+1 by NAT_1:22;
     i < i+1 by REAL_1:69;
   then A24:   not i in X by A22,A23;
A25: not i+1 in Y by A4,A21,A23,XBOOLE_0:3;
     i+1 < n by A21,A23,Th23;
   then A26:  [i,i+1] in the InternalRel of Necklace n by Th22;
     now per cases by A5,A26,XBOOLE_0:def 2;
    suppose [i,i+1] in (the InternalRel of Necklace n) |_2 Y;
     then [i,i+1] in [:Y,Y:] by WELLORD1:16;
    hence contradiction by A25,ZFMISC_1:106;
    suppose [i,i+1] in (the InternalRel of Necklace n) |_2 X;
     then [i,i+1] in [:X,X:] by WELLORD1:16;
    hence contradiction by A24,ZFMISC_1:106;
   end;
   hence thesis;
end;

theorem
Th25:  for i,j being natural number st [i,j] in the InternalRel of Necklace n
       holds i = j + 1 or j = i + 1
proof
  let i,j be natural number such that
      A1: [i,j] in the InternalRel of Necklace n;
    [i,j] in
   {[k,k+1] where k is Nat:k+1 < n} \/ {[l+1,l] where l is Nat:l+1 < n}
        by A1,Th19;
  then A2: [i,j] in {[k,k+1] where k is Nat:k+1 < n} or
     [i,j] in {[k+1,k] where k is Nat:k+1 < n} by XBOOLE_0:def 2;
    i + 1 = j or j + 1 = i
   proof
    per cases by A2;
    suppose ex k being Nat st [i,j] = [k,k+1] & k+1 < n;
     then consider k such that
A3:    [i,j] = [k,k+1] and k+1 < n;
       i = k & j = k+1 by A3,ZFMISC_1:33;
    hence thesis;
    suppose (ex k being Nat st [i,j] = [k+1,k] & k+1 < n);
     then consider k such that
A4:   [i,j] = [k+1,k] and k+1 < n;
        i = k+1 & j = k by A4,ZFMISC_1:33;
     hence thesis;
   end;
  hence thesis;
end;

theorem
Th26:   for i,j being natural number st (i = j + 1 or j = i + 1) &
   i in the carrier of Necklace n & j in the carrier of Necklace n
   holds [i,j] in the InternalRel of Necklace n
proof
 let i,j be natural number such that A1:  i = j + 1 or j = i + 1 and
A2:  i in the carrier of Necklace n and
A3:  j in the carrier of Necklace n;
  per cases by A1;
  suppose
A4:  i=j+1;
   then j+1 < n by A2,Th23;
   then [j,j+1] in the InternalRel of Necklace n by Th22;
   then [j+1,j] in (the InternalRel of Necklace n)~ by RELAT_1:def 7;
  hence thesis by A4,RELAT_2:30;
  suppose
A5:  j=i+1;
  then i+1 < n by A3,Th23;
  hence thesis by A5,Th22;
end;

theorem
Th27:   n > 0 implies Card ({[i+1,i] where i is Nat:i+1 < n}) = n-1
  proof
  assume
A1: n > 0;
    then A2: n >= 0+1 by NAT_1:38;
A3:   i in n-'1 implies i+1<n
     proof
      assume i in n-'1;
      then A4:i < n-'1 by EULER_1:1;
        n >= 0+1 by A1,NAT_1:38;
      then i < n-1 by A4,SCMFSA_7:3;
     hence thesis by REAL_1:86;
     end;
     deffunc F(Nat) = [$1+1,$1];
     defpred P[Nat] means $1+1<n;
     defpred Q[Nat] means $1 in n-'1;
A5: for i being Nat holds P[i] iff Q[i]  proof let i being Nat;
    thus i+1<n implies i in n-'1
     proof
      assume i+1<n;
      then i < n-1 by REAL_1:86;
      then i < n-'1 by A2,SCMFSA_7:3;
      hence thesis by EULER_1:1;
     end;
    thus thesis by A3;
   end;
A6:   {F(i) where i is Nat: P[i]}
    = {F(i) where i is Nat: Q[i]} from Fraenkel6'(A5);
A7: n-'1 c= NAT by ORDINAL1:def 2;
A8: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1=d2 by ZFMISC_1:33;
  n-'1, {F(i) where i is Nat: i in n-'1} are_equipotent from CardMono'(A7,A8);
  hence Card ({[i+1,i] where i is Nat:i+1 < n})
          = Card (n-'1) by A6,CARD_1:21
          .= n-'1 by CARD_1:66
          .= n-1 by A2,SCMFSA_7:3;
  end;

theorem
Th28:   n > 0 implies Card the InternalRel of Necklace n = 2*(n-1)
  proof
   assume A1: n > 0;
    then A2: n >= 0+1 by NAT_1:38;
    deffunc F(Nat) = $1;
    deffunc G(Nat) = $1+1;
    defpred P[Nat] means $1+1 < n;
   set A = {[i,i+1] where i is Nat:i+1 < n},
       B = {[G(i),F(i)] where i is Nat:P[i]};
A3:   the InternalRel of Necklace n = A \/ B by Th19;
     A = the InternalRel of n-SuccRelStr by Def7;
   then Card A = n-1 by A1,Th17;
      then A4: Card A = Card (n-1) by CARD_1:def 5;
        Card B = n-1 by A1,Th27;
      then A5: Card B = Card (n-1) by CARD_1:def 5;
     A is Relation-like
    proof
     let x be set;
     assume x in A;
     then ex i being Nat st x = [i,i+1] & i+1<n;
     hence thesis;
    end;
   then reconsider A as Relation;
A6:   A = {[F(i),G(i)] where i is Nat: P[i]};
A7:  A~ = B from Convers(A6);
A8:   A misses B
      proof
       assume A meets B;
       then consider x being set such that
A9:     x in A and
A10:     x in B by XBOOLE_0:3;
       consider y,z being set such that
A11:      x = [y,z] by A9,RELAT_1:def 1;
A12:      [z,y] in A by A7,A10,A11,RELAT_1:def 7;
       consider i be Nat such that
A13:      [y,z] = [i,i+1] & i+1<n by A9,A11;
A14:      y = i & z = i+1 by A13,ZFMISC_1:33;
       consider j be Nat such that
A15:      [z,y] = [j,j+1] & j+1<n by A12;
         z = j & y = j+1 by A15,ZFMISC_1:33;
       then i+1+1 < i+1 by A14,NAT_1:38;
       hence contradiction by NAT_1:29;
      end;
A16: n-'1 = n-1 by A2,SCMFSA_7:3;
     Card the InternalRel of Necklace n
                       = Card (n-1) +` Card (n-1) by A3,A4,A5,A8,CARD_2:48
                       .= Card ((n-'1) + (n-'1)) by A16,CARD_2:51
                       .= (n-'1) + (n-'1) by CARD_1:66
                       .= 2*(n-1) by A16,XCMPLX_1:11;
   hence Card the InternalRel of Necklace n = 2*(n-1);
  end;

theorem
     Necklace 1, ComplRelStr Necklace 1 are_isomorphic
 proof
  set S = Necklace 1,
      T = ComplRelStr S;
  set f = 0 .--> 0;
A1:  dom f = {0} by CQC_LANG:5
       .= the carrier of S by Th21,CARD_5:1;
A2:  the carrier of S = {0} by Th21,CARD_5:1;
A3:  the carrier of S = the carrier of T by Def9;
    f = {0} --> 0 by CQC_LANG:def 2
    .= [:{0},{0}:] by FUNCOP_1:def 2;
  then f is Function of the carrier of S, the carrier of T
                                 by A1,A2,A3,FUNCT_2:def 1,RELSET_1:def 1;
  then reconsider g = f as map of S,T;
A4:    dom g = {0} by CQC_LANG:5;
A5:  rng g = {0} by CQC_LANG:5;
A6:  g is monotone
      proof
       let x,y being Element of S such that
A7:    x <= y;
         the carrier of S = 1 by Th21;
       then reconsider i = x, j = y as natural number by Th4;
     [x,y] in the InternalRel of S by A7,ORDERS_1:def 9;
then A8:    i = j + 1 or j = i + 1 by Th25;
       let a,b being Element of T such that
         a = g.x & b = g.y;
A9:     the carrier of S = {0} by Th21,CARD_5:1;
then A10:       x = 0 by TARSKI:def 1;
        y = 0 by A9,TARSKI:def 1;
       hence thesis by A8,A10;
      end;
   g = g"
      proof
     for y,x being set holds y in rng g & x = g.y iff x in dom g & y = g.x
        proof
         let x,y being set;
A11:    y in rng g & x = g.y implies x in dom g & y=g.x
        proof
         assume that
A12:      y in rng g and
A13:      x = g.y;
         A14: y = 0 by A5,A12,TARSKI:def 1;
         then x = 0 by A13,CQC_LANG:6;
         hence thesis by A4,A14,CQC_LANG:6,TARSKI:def 1;
        end;
     x in dom g & y=g.x implies y in rng g & x = g.y
        proof
         assume that
A15:        x in dom g and
A16:        y = g.x;
         the carrier of S = {0} by Th21,CARD_5:1;
          then A17: x = 0 by A15,TARSKI:def 1;
          then y = 0 by A16,CQC_LANG:6;
          hence thesis by A5,A17,CQC_LANG:6,TARSKI:def 1;
         end;
         hence thesis by A5,A11,CQC_LANG:5;
        end;
       hence thesis by A4,A5,FUNCT_1:54;
      end;
  then reconsider h = g" as map of T,S by A3;
    h is monotone
   proof
    let x,y being Element of T such that
A18:    x <= y;
A19:   the carrier of T = 1 by A3,Th21;
    then reconsider i = x, j = y as natural number by Th4;
      [x,y] in the InternalRel of T by A18,ORDERS_1:def 9;
    then [x,y] in (the InternalRel of S)` \ id (the carrier of S)
                                                         by Def9;
then not [x,y] in id (the carrier of S) by XBOOLE_0:def 4;
then A20:  (not x in (the carrier of S) or x <> y) by RELAT_1:def 10;
A21:  x in (the carrier of T) & y in (the carrier of T);
     A22: i = 0 by A19,CARD_5:1,TARSKI:def 1;
     A23: j = 0 by A19,CARD_5:1,TARSKI:def 1;
A24:  i + 1 <> j & j + 1 <> i & i <> j
       proof
        hereby assume A25: i+1=j or j+1=i;
         per cases by A25;
         suppose i+1 = j;
         hence contradiction by A19,A22,EULER_1:1;
         suppose j+1=i;
         hence contradiction by A19,A23,EULER_1:1;
        end;
       thus i <> j by A20,A21,Def9;
       end;
      let a,b being Element of S such that
        a = h.x & b = h.y;
A26:    the carrier of T = {0} by A3,Th21,CARD_5:1;
      y = 0 by A19,CARD_5:1,TARSKI:def 1;
      hence thesis by A24,A26,TARSKI:def 1;
   end;
  then g is isomorphic by A6,WAYBEL_0:def 38;
  hence thesis by WAYBEL_1:def 8;
 end;

theorem
     Necklace 4, ComplRelStr Necklace 4 are_isomorphic
  proof
   set S = Necklace 4,
       T = ComplRelStr Necklace 4;
   set g = (0,1) --> (1,3), h = (2,3) --> (0,2),
       f = g +* h;
A1:  dom f = dom (0,1) --> (1,3) \/ dom (2,3) --> (0,2) by FUNCT_4:def 1
  .= {0,1} \/ dom (2,3) --> (0,2) by FUNCT_4:65
  .= {0,1} \/ {2,3} by FUNCT_4:65
  .= {0,1,2,3} by ENUMSET1:45;
  then A2: dom f = the carrier of S by Th2,Th21;
A3:  rng g = {1,3} by FUNCT_4:67;
A4:  rng h = {0,2} by FUNCT_4:67;
     rng f c= the carrier of T
   proof
     let x be set;
     assume
A5:  x in rng f;
A6:  rng f c= rng g \/ rng h by FUNCT_4:18;
       rng g \/ rng h = {1,3,0,2} by A3,A4,ENUMSET1:45
     .= {0,1,2,3} by ENUMSET1:112;
     then x in 4 by A5,A6,Th2;
     then x in the carrier of S by Th21;
     hence x in the carrier of T by Def9;
   end;
  then f is Function of the carrier of S,
                         the carrier of T by A2,FUNCT_2:def 1,RELSET_1:11;
  then reconsider f as map of S,T;
   take f;
   per cases;
   case that
     S is non empty and
     T is non empty;
A7:   g is one-to-one
    proof
A8:     g = ({0} --> 1) +* ({1} -->3) by FUNCT_4:def 4;
A9:     {0} --> 1 = 0 .--> 1 by CQC_LANG:def 2;
A10:     {1} --> 3 = 1 .--> 3 by CQC_LANG:def 2;
       rng (0 .--> 1) misses rng (1 .--> 3)
     proof
     assume rng (0 .--> 1) meets rng (1 .--> 3);
     then consider x being set such that
A11:     x in rng (0 .--> 1) & x in rng (1 .--> 3) by XBOOLE_0:3;
A12:     rng (0 .--> 1) = {1} by CQC_LANG:5;
A13:     rng (1 .--> 3) = {3} by CQC_LANG:5;
       x = 1 by A11,A12,TARSKI:def 1;
      hence contradiction by A11,A13,TARSKI:def 1;
     end;
    hence thesis by A8,A9,A10,KNASTER:1;
    end;
A14: h is one-to-one
    proof
A15:     h = ({2} --> 0) +* ({3} -->2) by FUNCT_4:def 4;
A16:     {2} --> 0 = 2 .--> 0 by CQC_LANG:def 2;
A17:     {3} --> 2 = 3 .--> 2 by CQC_LANG:def 2;
       rng (2 .--> 0) misses rng (3 .--> 2)
     proof
      assume rng (2 .--> 0) meets rng (3 .--> 2);
      then consider x being set such that
A18:     x in rng (2 .--> 0) & x in rng (3 .--> 2) by XBOOLE_0:3;
A19:     rng (2 .--> 0) = {0} by CQC_LANG:5;
A20:     rng (3 .--> 2) = {2} by CQC_LANG:5;
          x = 0 by A18,A19,TARSKI:def 1;
      hence contradiction by A18,A20,TARSKI:def 1;
     end;
    hence thesis by A15,A16,A17,KNASTER:1;
    end;
A21:     dom g misses dom h
      proof
       assume dom g meets dom h;
       then consider x being set such that
A22:      x in dom g & x in dom h by XBOOLE_0:3;
         (x = 0 or x = 1) & (x = 2 or x = 3) by A22,TARSKI:def 2;
       hence contradiction;
      end;
A23:    rng g misses rng h
     proof
      assume rng g meets rng h;
      then consider x being set such that
A24:     x in rng g & x in rng h by XBOOLE_0:3;
         (x = 1 or x = 3) & (x = 0 or x = 2) by A3,A4,A24,TARSKI:def 2;
       hence contradiction;
     end;
    hence A25: f is one-to-one by A7,A14,KNASTER:1;
     set A = the InternalRel of T;
     set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
A26:    B c= A
      proof
       let x be set;
       assume x in B;
then A27:       x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3]
or
         x = [3,0] by ENUMSET1:28;
       set C = the carrier of S;
         0 in C & 1 in C & 2 in C & 3 in C by A1,A2,ENUMSET1:19;
       then reconsider x'=x as Element of [:C,C:] by A27,ZFMISC_1:106;
A28:     x' in (the InternalRel of S)`
        proof
           not x' in the InternalRel of S
         proof
          assume x' in the InternalRel of S;
          then consider i being Nat such that
            i+1< 4 and
A29:           x'= [i,i+1] or x'= [i+1,i] by Th20;
            i=1 & i+1=3 or i=3 & i+1=1 or i=0 & i+1=2 or i=2 & i+1=0 or
          i=0 & i+1=3 or i=3 & i+1=0 by A27,A29,ZFMISC_1:33;
          hence contradiction;
         end;
         hence x' in (the InternalRel of S)` by SUBSET_1:50;
        end;
         not x in id (the carrier of S) by A27,RELAT_1:def 10;
       then x in (the InternalRel of S)` \
             id (the carrier of S) by A28,XBOOLE_0:def 4;
       hence thesis by Def9;
      end;
    thus f is monotone
    proof
     let x,y being Element of S such that
A30:    x <= y;
       the carrier of S = 4 by Th21;
     then reconsider i = x, j = y as natural number by Th4;
      [x,y] in the InternalRel of S by A30,ORDERS_1:def 9;
then A31:    i = j + 1 or j = i + 1 by Th25;
     let a,b being Element of T such that
A32:     a = f.x & b = f.y;
A33:     dom g = {0,1} by FUNCT_4:65;
A34:     dom h = {2,3} by FUNCT_4:65;
A35:     0 in dom g by A33,TARSKI:def 2;
A36:     1 in dom g by A33,TARSKI:def 2;
A37:     2 in dom h by A34,TARSKI:def 2;
A38:     3 in dom h by A34,TARSKI:def 2;
A39:     f.0 = g.0 by A21,A35,FUNCT_4:17
         .= 1 by FUNCT_4:66;
A40:     f.1 = g.1 by A21,A36,FUNCT_4:17
         .= 3 by FUNCT_4:66;
A41:     f.2 = h.2 by A37,FUNCT_4:14
         .= 0 by FUNCT_4:66;
A42:     f.3 = h.3 by A38,FUNCT_4:14
         .= 2 by FUNCT_4:66;
     per cases by A1,A2,ENUMSET1:18;
     suppose x = 0 & y = 0;
     hence a <= b by A31;
     suppose x = 0 & y = 1;
      then [a,b] in B by A32,A39,A40,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 0 & y = 2;
     hence a <= b by A31;
     suppose x = 0 & y = 3;
     hence a <= b by A31;
     suppose x = 1 & y = 0;
      then [a,b] in B by A32,A39,A40,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 1 & y = 1;
     hence a <= b by A31;
     suppose x = 1 & y = 2;
      then [a,b] in B by A32,A40,A41,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 1 & y = 3;
     hence a <= b by A31;
     suppose x = 2 & y = 0;
     hence a <= b by A31;
     suppose x = 2 & y = 1;
      then [a,b] in B by A32,A40,A41,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 2 & y = 2;
     hence a <= b by A31;
     suppose x = 2 & y = 3;
      then [a,b] in B by A32,A41,A42,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 3 & y = 0;
     hence a <= b by A31;
     suppose x = 3 & y = 1;
     hence a <= b by A31;
     suppose x = 3 & y = 2;
      then [a,b] in B by A32,A41,A42,ENUMSET1:29;
     hence a <= b by A26,ORDERS_1:def 9;
     suppose x = 3 & y = 3;
     hence a <= b by A31;
    end;
      rng f = rng g \/ rng h by A21,Th7
         .= {1,3,0,2} by A3,A4,ENUMSET1:45
         .= {0,1,2,3} by ENUMSET1:112
         .= the carrier of S by Th2,Th21
         .= the carrier of T by Def9;
    then f" is Function of the carrier of T,the carrier of S
         by A25,FUNCT_2:31;
    then reconsider F = f" as map of T,S;
    take F;
    thus F = f";
    thus F is monotone
     proof
      let x,y being Element of T such that
A43:    x <= y;
A44:   the carrier of T = the carrier of S by Def9
                       .= 4 by Th21;
     then x is natural & y is natural by Th4;
     then reconsider i = x, j = y as Nat by ORDINAL2:def 21;
       [x,y] in the InternalRel of T by A43,ORDERS_1:def 9;
     then A45:[x,y] in (the InternalRel of S)` \ id (the carrier of S)
          by Def9;
       [x,y] in (the InternalRel of S)` implies
           not [x,y] in (the InternalRel of S) by SUBSET_1:54;
     then not [x,y] in
      ({[k,k+1] where k is Nat:k+1 < 4} \/ {[l+1,l] where l is Nat:l+1 < 4})
       & not [x,y] in id (the carrier of S) by A45,Th19,XBOOLE_0:def 4;
     then A46: not [x,y] in {[k,k+1] where k is Nat:k+1 < 4} &
               not [x,y] in {[k+1,k] where k is Nat:k+1 < 4} by XBOOLE_0:def 2;
     not [x,y] in id (the carrier of S) by A45,XBOOLE_0:def 4;
then A47:    (not x in (the carrier of S) or x <> y) by RELAT_1:def 10;
A48:    x in (the carrier of T) & y in (the carrier of T);
A49:  i + 1 <> j & j + 1 <> i & i <> j
       proof
        hereby assume A50: i+1=j or j+1=i;
         per cases by A50;
         suppose
A51:         i+1 = j;
         then i+1 < 4 by A44,EULER_1:1;
         hence contradiction by A46,A51;
         suppose
A52:            j+1=i;
         then j+1 < 4 by A44,EULER_1:1;
         hence contradiction by A46,A52;
        end;
       thus i <> j by A47,A48,Def9;
       end;
     let a,b being Element of S such that
A53:     a = F.x & b = F.y;
A54:     g" = (1,3) --> (0,1) by Th11;
A55:     h" = (0,2) --> (2,3) by Th11;
A56:     dom (g") = {1,3} by A54,FUNCT_4:65;
A57:     dom (h") = {0,2} by A55,FUNCT_4:65;
      A58: dom (g") misses dom (h")
      proof
       assume dom (g") meets dom (h");
       then consider x being set such that
A59:      x in dom (g") & x in dom (h") by XBOOLE_0:3;
         (x = 1 or x = 3) & (x = 0 or x = 2) by A56,A57,A59,TARSKI:def 2;
       hence contradiction;
      end;
A60:     1 in dom (g") by A56,TARSKI:def 2;
A61:     3 in dom (g") by A56,TARSKI:def 2;
A62:     0 in dom (h") by A57,TARSKI:def 2;
A63:     2 in dom (h") by A57,TARSKI:def 2;
A64:     F.1 = (g" +* h").1 by A7,A14,A21,A23,Th8
           .= g".1 by A58,A60,FUNCT_4:17
           .= 0 by A54,FUNCT_4:66;
A65:     F.3 = (g" +* h").3 by A7,A14,A21,A23,Th8
           .= g".3 by A58,A61,FUNCT_4:17
           .= 1 by A54,FUNCT_4:66;
A66:     F.0 = (g" +* h").0 by A7,A14,A21,A23,Th8
           .= h".0 by A62,FUNCT_4:14
           .= 2 by A55,FUNCT_4:66;
A67:     F.2 = (g" +* h").2 by A7,A14,A21,A23,Th8
           .= h".2 by A63,FUNCT_4:14
           .= 3 by A55,FUNCT_4:66;
     per cases by A44,Th2,ENUMSET1:18;
     suppose x = 0 & y = 0;
     hence a <= b by A49;
     suppose x = 0 & y = 1;
     hence a <= b by A49;
     suppose x = 0 & y = 2;
      then a = 2 & b = 2+1 by A53,A66,A67;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 0 & y = 3;
      then a = 1+1 & b = 1 by A53,A65,A66;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 1 & y = 0;
     hence a <= b by A49;
     suppose x = 1 & y = 1;
     hence a <= b by A49;
     suppose x = 1 & y = 2;
     hence a <= b by A49;
     suppose x = 1 & y = 3;
      then a = 0 & b = 0+1 by A53,A64,A65;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 2 & y = 0;
      then a = 2+1 & b = 2 by A53,A66,A67;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 2 & y = 1;
     hence a <= b by A49;
     suppose x = 2 & y = 2;
     hence a <= b by A49;
     suppose x = 2 & y = 3;
     hence a <= b by A49;
     suppose x = 3 & y = 0;
      then a = 1 & b = 1+1 by A53,A65,A66;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 3 & y = 1;
      then a = 0+1 & b = 0 by A53,A64,A65;
      then [a,b] in the InternalRel of S by Th26;
     hence a <= b by ORDERS_1:def 9;
     suppose x = 3 & y = 2;
     hence a <= b by A49;
     suppose x = 3 & y = 3;
     hence a <= b by A49;
    end;
   case S is empty or T is empty;
   hence thesis;
  end;

theorem
     Necklace n, ComplRelStr Necklace n are_isomorphic implies
   n = 0 or n = 1 or n = 4
 proof
  assume
A1:  Necklace n, ComplRelStr Necklace n are_isomorphic;
  assume A2:not thesis;
  per cases by A2,CQC_THE1:5;
  suppose A3: n=2;
   set S = Necklace 2,
       T = ComplRelStr S;
   set X = {[0,1],[1,0]},
       Y = the InternalRel of S;
   A4: Card (the InternalRel of S) = 2*(2-1) by Th28
                                   .= 2;
A5:   the InternalRel of S =
  {[i,i+1] where i is Nat:i+1 < 2} \/ {[i+1,i] where i is Nat:i+1 < 2} by Th19;
   A6: [0,0+1] in {[i,i+1] where i is Nat:i+1 < 2};
   A7: [0+1,0] in {[i+1,i] where i is Nat:i+1 < 2};
A8:   X c= Y
    proof
     let x be set;
     assume A9: x in {[0,1],[1,0]};
     per cases by A9,TARSKI:def 2;
     suppose x = [0,1];
     hence thesis by A5,A6,XBOOLE_0:def 2;
     suppose x = [1,0];
     hence thesis by A5,A7,XBOOLE_0:def 2;
    end;
A10:   Y c= X
    proof
     let x be set;
     assume A11: x in Y;
     then consider y,z being set such that
A12:      x = [y,z] by RELAT_1:def 1;
     per cases by A5,A11,XBOOLE_0:def 2;
     suppose x in {[i,i+1] where i is Nat:i+1 < 2};
     then consider i be Nat such that
A13:      [y,z] = [i,i+1] & i+1 < 2 by A12;
A14:      y = i & z = i+1 by A13,ZFMISC_1:33;
       i+1 < 1+1 by A13;
     then i < 0+1 by REAL_1:55;
     then i <= 0 by NAT_1:38;
     then y = 0 by A14,NAT_1:19;
     hence thesis by A12,A14,TARSKI:def 2;
     suppose x in {[i+1,i] where i is Nat:i+1 < 2};
     then consider i be Nat such that
A15:      [y,z] = [i+1,i] & i+1 < 2 by A12;
A16:      y = i+1 & z = i by A15,ZFMISC_1:33;
       i+1 < 1+1 by A15;
     then i < 0+1 by REAL_1:55;
     then i <= 0 by NAT_1:38;
     then z = 0 by A16,NAT_1:19;
     hence thesis by A12,A16,TARSKI:def 2;
    end;
then A17:    X = Y by A8,XBOOLE_0:def 10;
     the InternalRel of T is empty
    proof
     assume the InternalRel of T is non empty;
     then consider x being set such that
A18:    x in (the InternalRel of T) by XBOOLE_0:def 1;
       x in (the InternalRel of S)` \ id (the carrier of S) by A18,Def9;
     then A19:x in (the InternalRel of S)` &
          not x in id (the carrier of S) by XBOOLE_0:def 4;
A20:     the carrier of S = the carrier of SymRelStr(2-SuccRelStr) by Def10
                    .= the carrier of 2-SuccRelStr by Def8
                    .= {0,1} by Def7,CARD_5:1;
A21:   id (the carrier of S) = {[0,0],[1,1]}
        proof
A22:      id (the carrier of S) c= {[0,0],[1,1]}
          proof
           let x be set;
           assume A23: x in id (the carrier of S);
           then consider x1,x2 being set such that
A24:           x = [x1,x2] by RELAT_1:def 1;
A25:          x1 in {0,1} & x1 = x2 by A20,A23,A24,RELAT_1:def 10;
          then x1 = 0 or x1 = 1 by TARSKI:def 2;
          hence thesis by A24,A25,TARSKI:def 2;
          end;
           {[0,0],[1,1]} c= id (the carrier of S)
          proof
           let x be set;
           assume x in {[0,0],[1,1]};
           then A26:x = [0,0] or x = [1,1] by TARSKI:def 2;
             0 in the carrier of S & 1 in the carrier of S by A20,TARSKI:def 2;
           hence thesis by A26,RELAT_1:def 10;
          end;
          hence thesis by A22,XBOOLE_0:def 10;
        end;
A27:     (the InternalRel of S)` = [:the carrier of S,the carrier of S:] \
      (the InternalRel of S) by SUBSET_1:def 5;
   (the InternalRel of S)` = id (the carrier of S)
       proof
        thus (the InternalRel of S)` c= id (the carrier of S)
         proof
          let x be set;
          assume x in (the InternalRel of S)`;
          then A28:x in [:the carrier of S,the carrier of S:] &
               not x in (the InternalRel of S) by A27,XBOOLE_0:def 4;
          then x in {[0,0],[0,1],[1,0],[1,1]} by A20,MCART_1:25;
          then x = [0,0] or x = [0,1] or x = [1,0] or x = [1,1]
               by ENUMSET1:18;
          hence thesis by A17,A21,A28,TARSKI:def 2;
         end;
        let x be set;
        assume A29: x in id the carrier of S;
        then A30: x = [0,0] or x = [1,1] by A21,TARSKI:def 2;
          not x in the InternalRel of S
         proof
          per cases by A21,A29,TARSKI:def 2;
          suppose A31: x = [0,0];
          then A32:        x <> [0,1] by ZFMISC_1:33;
             x <> [1,0] by A31,ZFMISC_1:33;
          hence thesis by A10,A32,TARSKI:def 2;
          suppose A33: x = [1,1];
          then A34:        x <> [0,1] by ZFMISC_1:33;
             x <> [1,0] by A33,ZFMISC_1:33;
          hence thesis by A10,A34,TARSKI:def 2;
         end;
        then x in {[0,0],[0,1],[1,0],[1,1]} &
             not x in the InternalRel of S by A30,ENUMSET1:19;
       then x in [:the carrier of S,the carrier of S:] &
            (not x in the InternalRel of S) by A20,MCART_1:25;
       then x in ([:the carrier of S,the carrier of S:] \
            (the InternalRel of S) ) by XBOOLE_0:def 4;
       hence thesis by SUBSET_1:def 5;
       end;
     hence contradiction by A19;
    end;
   hence contradiction by A1,A3,A4,Th18,CARD_1:47;
  suppose A35: n=3;
   set S = Necklace 3,
       T = ComplRelStr S;
   set X = {[0,1],[1,0],[1,2],[2,1]},
       Y = the InternalRel of S;
   A36: the carrier of S = {0,1,2} by Th21,YELLOW11:1;
   A37: Card (the InternalRel of S) = 2*(3-1) by Th28
                                   .= 4;
A38:   the InternalRel of S =
  {[i,i+1] where i is Nat:i+1 < 3} \/ {[i+1,i] where i is Nat:i+1 < 3} by Th19;
    A39: [0,0+1] in {[i,i+1] where i is Nat:i+1 < 3};
    A40: [0+1,0] in {[i+1,i] where i is Nat:i+1 < 3};
    A41: [0+1,1+1] in {[i,i+1] where i is Nat:i+1 < 3};
    A42: [1+1,0+1] in {[i+1,i] where i is Nat:i+1 < 3};
A43:   X c= Y
    proof
     let x be set;
     assume A44: x in X;
     per cases by A44,ENUMSET1:18;
     suppose x = [0,1];
     hence thesis by A38,A39,XBOOLE_0:def 2;
     suppose x = [1,0];
     hence thesis by A38,A40,XBOOLE_0:def 2;
     suppose x = [1,2];
     hence thesis by A38,A41,XBOOLE_0:def 2;
     suppose x = [2,1];
     hence thesis by A38,A42,XBOOLE_0:def 2;
    end;
    Y c= X
    proof
     let x be set;
     assume A45: x in Y;
     then consider y,z being set such that
A46:      x = [y,z] by RELAT_1:def 1;
     per cases by A38,A45,XBOOLE_0:def 2;
     suppose x in {[i,i+1] where i is Nat:i+1 < 3};
     then consider i be Nat such that
A47:      [y,z] = [i,i+1] & i+1 < 3 by A46;
A48:      y = i & z = i+1 by A47,ZFMISC_1:33;
       i+1 < 1+2 by A47;
     then i < 1 + 1 by REAL_1:55;
     then i <= 1 by NAT_1:38;
     then y = 0 or y = 1 by A48,CQC_THE1:2;
     hence thesis by A46,A48,ENUMSET1:19;
     suppose x in {[i+1,i] where i is Nat:i+1 < 3};
     then consider i be Nat such that
A49:      [y,z] = [i+1,i] & i+1 < 3 by A46;
A50:      y = i+1 & z = i by A49,ZFMISC_1:33;
       i+1 < 1+2 by A49;
     then i < 1 + 1 by REAL_1:55;
     then i <= 1 by NAT_1:38;
     then z = 0 or z = 1 by A50,CQC_THE1:2;
     hence thesis by A46,A50,ENUMSET1:19;
    end;
then A51:  X = Y by A43,XBOOLE_0:def 10;
A52:  id (the carrier of S) = {[0,0],[1,1],[2,2]}
      proof
A53:    id (the carrier of S) c= {[0,0],[1,1],[2,2]}
         proof
           let x be set;
           assume A54: x in id (the carrier of S);
           then consider x1,x2 being set such that
A55:           x = [x1,x2] by RELAT_1:def 1;
A56:          x1 in {0,1,2} & x1 = x2 by A36,A54,A55,RELAT_1:def 10;
          then x1 = 0 or x1 = 1 or x1 = 2 by ENUMSET1:13;
          hence thesis by A55,A56,ENUMSET1:14;
         end;
         {[0,0],[1,1],[2,2]} c= id (the carrier of S)
         proof
           let x be set;
           assume A57: x in {[0,0],[1,1],[2,2]};
           per cases by A57,ENUMSET1:def 1;
           suppose A58: x = [0,0] or x = [1,1];
             0 in the carrier of S & 1 in the carrier of S by A36,ENUMSET1:def
1
;
           hence thesis by A58,RELAT_1:def 10;
           suppose A59: x = [2,2];
             2 in the carrier of S by A36,ENUMSET1:def 1;
           hence thesis by A59,RELAT_1:def 10;
          end;
         hence thesis by A53,XBOOLE_0:def 10;
        end;
A60:   the InternalRel of T = (the InternalRel of S)` \
             id (the carrier of S) by Def9;
A61:  (the InternalRel of S)` = [:the carrier of S,the carrier of S:] \
                               (the InternalRel of S) by SUBSET_1:def 5;
A62:  [:the carrier of S,the carrier of S:] =
         {[0,0],[0,1],[0,2],[1,0],[1,1],[1,2],[2,0],[2,1],[2,2]} by A36,Th3;
A63:  (the InternalRel of S)` = {[0,2],[2,0],[0,0],[1,1],[2,2]}
     proof
      thus (the InternalRel of S)` c= {[0,2],[2,0],[0,0],[1,1],[2,2]}
       proof
        let x be set;
        assume x in (the InternalRel of S)`;
        then x in {[0,0],[0,1],[0,2],[1,0],[1,1],[1,2],[2,0],[2,1],[2,2]} &
         not x in {[0,1],[1,0],[1,2],[2,1]} by A43,A61,A62,XBOOLE_0:def 4;
       then x in {[0,0],[0,1],[0,2],[1,0],[1,1],[1,2],[2,0],[2,1],[2,2]} &
         x <> [0,1] & x <> [1,0] & x <> [1,2] & x <> [2,1] by ENUMSET1:19;
       then x = [0,2] or x = [2,0] or x = [0,0] or x = [1,1] or x = [2,2]
                by BVFUNC24:26;
        hence thesis by ENUMSET1:24;
       end;
      let x be set;
      assume x in {[0,2],[2,0],[0,0],[1,1],[2,2]};
then A64:    x = [0,2] or x = [2,0] or x = [0,0] or x = [1,1] or x = [2,2]
                                        by ENUMSET1:23;
      then x <> [0,1] & x <> [1,0] & x <> [1,2] & x <> [2,1] by ZFMISC_1:33;
      then A65: not x in {[0,1],[1,0],[1,2],[2,1]} by ENUMSET1:18;
        x in {[0,0],[0,1],[0,2],[1,0],[1,1],[1,2],[2,0],[2,1],[2,2]}
              by A64,BVFUNC24:49;
      hence thesis by A51,A61,A62,A65,XBOOLE_0:def 4;
     end;
A66:  the InternalRel of T = {[0,2],[2,0]}
   proof
    thus the InternalRel of T c= {[0,2],[2,0]}
     proof
      let x be set;
      assume x in the InternalRel of T;
      then A67: x in {[0,2],[2,0],[0,0],[1,1],[2,2]} &
           not x in {[0,0],[1,1],[2,2]} by A52,A60,A63,XBOOLE_0:def 4;
      then x = [0,2] or x = [2,0] or x = [0,0] or x =[1,1] or x = [2,2]
           by ENUMSET1:23;
      hence thesis by A67,ENUMSET1:14,TARSKI:def 2;
     end;
    let x be set;
    assume x in {[0,2],[2,0]};
    then A68: x = [0,2] or x =[2,0] by TARSKI:def 2;
    then A69: x in {[0,2],[2,0],[0,0],[1,1],[2,2]} by ENUMSET1:24;
        x <> [0,0] & x <> [1,1] & x <> [2,2] by A68,ZFMISC_1:33;
    then not x in {[0,0],[1,1],[2,2]} by ENUMSET1:13;
    hence thesis by A52,A60,A63,A69,XBOOLE_0:def 4;
   end;
     [0,2] <> [2,0] by ZFMISC_1:33;
   then Card (the InternalRel of T) = 2 by A66,CARD_2:76;
  hence thesis by A1,A35,A37,Th18;
  suppose A70: n > 4;
   set S = Necklace n,
       T = ComplRelStr S;
A71:  the carrier of S = n by Th21;
       n > 0 by A70,AXIOMS:22;
then A72:  Card the InternalRel of S = 2*(n-1) by Th28;
A73:     (the InternalRel of S)` = [:the carrier of S,the carrier of S:] \
      (the InternalRel of S) by SUBSET_1:def 5;
A74:    the carrier of S = n by Th21;
     n is Nat by ORDINAL2:def 21;
   then Card n = n by CARD_1:66;
   then Card [:n,n:] = n*n by CARD_2:65;
  then A75: Card (the InternalRel of S)` = n*n - 2*(n-1) by A72,A73,A74,CARD_2:
63;
         n is Nat by ORDINAL2:def 21;
    then n = Card n by CARD_1:66;
    then A76:  Card id (the carrier of S) = n by A71,Th6;
      id (the carrier of S) misses (the InternalRel of S)
     proof
      assume not thesis;
      then consider x being set such that
A77:    x in id (the carrier of S) and
A78:    x in the InternalRel of S by XBOOLE_0:3;
       consider x1,x2 being set such that
A79:       x = [x1,x2] by A77,RELAT_1:def 1;
      A80: x1=x2 by A77,A79,RELAT_1:def 10;
      consider i being Nat such that
        i+1 < n and
A81:      (x = [i,i+1] or x = [i+1,i]) by A78,Th20;
      per cases by A79,A81;
      suppose [x1,x2] = [i,i+1];
      then x1 = i & x2 = i+1 by ZFMISC_1:33;
      hence thesis by A80,NAT_1:38;
      suppose [x1,x2] = [i+1,i];
      then x1 = i+1 & x2 = i by ZFMISC_1:33;
      hence thesis by A80,NAT_1:38;
     end;
   then A82: id (the carrier of S) c= (the InternalRel of S)`
                                          by A73,XBOOLE_1:86;
  A83: Card (the InternalRel of T) =
       Card ((the InternalRel of S)` \ id (the carrier of S)) by Def9
    .= n*n - 2*(n-1) - n by A75,A76,A82,CARD_2:63;
      n*n - 2*(n-1) - n <> 2*(n-1)
     proof
      assume not thesis;
      then n*n - (2*n - 2*1) - n = 2*(n-1) by XCMPLX_1:40;
      then n*n - (2*n - 2) - n - 2*(n-1) = 0 by XCMPLX_1:14;
      then n*n - (2*n - 2) - n - (2*n - 2*1) = 0 by XCMPLX_1:40;
      then n*n - (2*n - 2) + (- n - (2*n - 2*1)) = 0 by XCMPLX_1:158;
      then n*n - (2*n - 2) + (-(2*n - 2) - n) = 0 by XCMPLX_1:144;
      then n*n - (2*n - 2) - (2*n - 2) - n = 0 by XCMPLX_1:158;
      then n*n - ((2*n - 2) + (2*n - 2)) - n = 0 by XCMPLX_1:36;
      then n*n - 2*(2*n - 2) - n = 0 by XCMPLX_1:11;
      then n*n - (2*(2*n) - 2*2) - n = 0 by XCMPLX_1:40;
      then n*n - (4*n - 4) - n = 0 by XCMPLX_1:4;
      then n*n - 4*n + 4 - n = 0 by XCMPLX_1:37;
      then n*n - 4*n - n + 4 = 0 by XCMPLX_1:29;
      then n*n - (4*n + n*1) + 4 = 0 by XCMPLX_1:36;
      then n*n - n*(4+1) + 4 = 0 by XCMPLX_1:8;
      then n ^2 - 5*n + 4 = 0 by SQUARE_1:def 3;
      then n ^2 + (- 5*n) + 4 = 0 by XCMPLX_0:def 8;
      then A84: 1*n ^2 + (- 5)*n + 4 = 0 by XCMPLX_1:175;
A85:   delta(1,-5,4) = (-5)^2 - 4*1*4 by QUIN_1:def 1
                    .= (-5)*(-5) - 4*4 by SQUARE_1:def 3
                    .= 9;
      then n = (- (-5) - sqrt delta(1,-5,4))/(2 * 1) or
            n = (- (-5) + sqrt delta(1,-5,4))/(2 * 1) by A84,QUIN_1:15;
       then n = (5 - sqrt (3*3))/2 or n = (5 + sqrt (3*3))/2 by A85;
       then n = (5 - sqrt 3^2)/2 or n = (5 + sqrt 3^2)/2 by SQUARE_1:def 3;
       then A86:n = (5 - 3)/2 or n = (5+3) /2 by SQUARE_1:89;
       per cases by A86;
       suppose n =1;
       hence contradiction by A70;
       suppose n=4;
       hence contradiction by A70;
     end;
  hence thesis by A1,A72,A83,Th18;
 end;


Back to top